![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp1bi | 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 |
---|---|
simp1bi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | 1 | biimpi 215 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp1d 1142 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: limord 6375 smores2 8292 smofvon2 8294 smofvon 8297 errel 8615 elunitrn 13338 lincmb01cmp 13366 iccf1o 13367 elfznn0 13488 elfzouz 13530 ef01bndlem 16026 sin01bnd 16027 cos01bnd 16028 sin01gt0 16032 cos01gt0 16033 sin02gt0 16034 gzcn 16764 mresspw 17432 drsprs 18152 ipodrscl 18387 subgrcl 18892 pmtrfconj 19207 pgpprm 19334 slwprm 19350 efgsdmi 19473 efgsrel 19475 efgs1b 19477 efgsp1 19478 efgsres 19479 efgsfo 19480 efgredlema 19481 efgredlemf 19482 efgredlemd 19485 efgredlemc 19486 efgredlem 19488 efgrelexlemb 19491 efgcpbllemb 19496 srgcmn 19879 ringgrp 19923 irredcl 20086 lmodgrp 20282 lssss 20350 phllvec 20986 obsrcl 21082 locfintop 22824 fclstop 23314 tmdmnd 23378 tgpgrp 23381 trgtgp 23471 tdrgtrg 23476 ust0 23523 ngpgrp 23907 elii1 24250 elii2 24251 icopnfcnv 24257 icopnfhmeo 24258 iccpnfhmeo 24260 xrhmeo 24261 oprpiece1res2 24267 phtpcer 24310 pcoval2 24331 pcoass 24339 clmlmod 24382 cphphl 24487 cphnlm 24488 cphsca 24495 bnnvc 24656 uc1pcl 25460 mon1pcl 25461 sinq12ge0 25817 cosq14ge0 25820 cosq34lt1 25835 cosord 25839 cos11 25841 recosf1o 25843 resinf1o 25844 efifo 25855 logrncn 25870 atanf 26182 atanneg 26209 efiatan 26214 atanlogaddlem 26215 atanlogadd 26216 atanlogsub 26218 efiatan2 26219 2efiatan 26220 tanatan 26221 areass 26261 dchrvmasumlem2 26798 dchrvmasumiflem1 26801 brbtwn2 27683 ax5seglem1 27706 ax5seglem2 27707 ax5seglem3 27709 ax5seglem5 27711 ax5seglem6 27712 ax5seglem9 27715 ax5seg 27716 axbtwnid 27717 axpaschlem 27718 axpasch 27719 axcontlem2 27743 axcontlem4 27745 axcontlem7 27748 pthistrl 28502 clwwlkbp 28758 sticl 30986 hstcl 30988 omndmnd 31738 slmdcmn 31866 orngring 31921 rrextnrg 32394 rrextdrg 32395 rossspw 32580 srossspw 32587 eulerpartlemd 32778 eulerpartlemf 32782 eulerpartlemgvv 32788 eulerpartlemgu 32789 eulerpartlemgh 32790 eulerpartlemgs2 32792 eulerpartlemn 32793 bnj564 33168 bnj1366 33253 bnj545 33319 bnj548 33321 bnj558 33326 bnj570 33329 bnj580 33337 bnj929 33360 bnj998 33381 bnj1006 33384 bnj1190 33432 bnj1523 33495 msrval 33944 mthmpps 33988 eqvrelrefrel 36998 atllat 37700 stoweidlem60 44202 fourierdlem111 44359 prproropf1o 45600 rngabl 46076 |
Copyright terms: Public domain | W3C validator |