![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp3bi | Structured version Visualization version GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp3bi | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | 1 | biimpi 206 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp3d 1095 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 df-3an 1056 |
This theorem is referenced by: limuni 5823 smores2 7496 ersym 7799 ertr 7802 fvixp 7955 undifixp 7986 fiint 8278 winalim2 9556 inar1 9635 supmullem1 11031 supmullem2 11032 supmul 11033 eluzle 11738 ico01fl0 12660 ef01bndlem 14958 sin01bnd 14959 cos01bnd 14960 sin01gt0 14964 divalglem6 15168 gznegcl 15686 gzcjcl 15687 gzaddcl 15688 gzmulcl 15689 gzabssqcl 15692 4sqlem4a 15702 prdsbasprj 16179 xpsff1o 16275 mreintcl 16302 drsdir 16982 subggrp 17644 pmtrfconj 17932 symggen 17936 psgnunilem1 17959 subgpgp 18058 slwispgp 18072 sylow2alem1 18078 oppglsm 18103 efgsdmi 18191 efgsrel 18193 efgsp1 18196 efgsres 18197 efgcpbllemb 18214 efgcpbl 18215 srgi 18557 srgrz 18572 srglz 18573 ringi 18606 ringsrg 18635 irredmul 18755 lmodlema 18916 lsscl 18991 phllmhm 20025 ipcj 20027 ipeq0 20031 ocvi 20061 obsip 20113 obsocv 20118 2ndcctbss 21306 locfinnei 21374 fclssscls 21869 tmdcn 21934 tgpinv 21936 trgtmd 22015 tdrgunit 22017 ngpds 22455 nrmtngdist 22508 elii1 22781 elii2 22782 icopnfcnv 22788 icopnfhmeo 22789 iccpnfhmeo 22791 xrhmeo 22792 phtpcer 22841 pcoass 22870 clmsubrg 22912 cphnmfval 23038 bnsca 23182 uc1pldg 23953 mon1pldg 23954 sinq12ge0 24305 cosq14gt0 24307 cosq14ge0 24308 sinord 24325 recosf1o 24326 resinf1o 24327 logrnaddcl 24366 logimul 24405 dvlog2lem 24443 atanf 24652 atanneg 24679 atancj 24682 efiatan 24684 atanlogaddlem 24685 atanlogadd 24686 atanlogsub 24688 efiatan2 24689 2efiatan 24690 ressatans 24706 dvatan 24707 areaf 24733 harmonicubnd 24781 harmonicbnd4 24782 lgamgulmlem2 24801 2sqlem2 25188 2sqlem3 25190 dchrvmasumiflem1 25235 pntpbnd2 25321 f1otrg 25796 f1otrge 25797 brbtwn2 25830 ax5seglem3 25856 axpaschlem 25865 axcontlem7 25895 hstel2 29206 stle1 29212 stj 29222 xrge0adddir 29820 omndadd 29834 slmdlema 29884 lmodslmd 29885 orngmul 29931 xrge0iifcnv 30107 xrge0iifiso 30109 xrge0iifhom 30111 rrextcusp 30177 rrextust 30180 unelros 30362 difelros 30363 inelsros 30369 diffiunisros 30370 sibfinima 30529 eulerpartlemf 30560 eulerpartlemgvv 30566 bnj563 30939 bnj1366 31026 bnj1379 31027 bnj554 31095 bnj557 31097 bnj570 31101 bnj594 31108 bnj1001 31154 bnj1006 31155 bnj1097 31175 bnj1177 31200 bnj1388 31227 bnj1398 31228 bnj1450 31244 bnj1501 31261 bnj1523 31265 snmlflim 31440 msrval 31561 mclsssvlem 31585 mclsind 31593 ptrecube 33539 cntotbnd 33725 heiborlem8 33747 dmnnzd 34004 atlex 34921 kelac1 37950 binomcxplemcvg 38870 binomcxplemnotnn0 38872 elixpconstg 39580 fvixp2 39703 stoweidlem39 40574 stoweidlem60 40595 fourierdlem40 40682 fourierdlem78 40719 isringrng 42206 |
Copyright terms: Public domain | W3C validator |