| 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 216 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
| 3 | 2 | simp1d 1143 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: limord 6444 smores2 8394 smofvon2 8396 smofvon 8399 errel 8754 elunitrn 13507 lincmb01cmp 13535 iccf1o 13536 elfznn0 13660 elfzouz 13703 ef01bndlem 16220 sin01bnd 16221 cos01bnd 16222 sin01gt0 16226 cos01gt0 16227 sin02gt0 16228 gzcn 16970 mresspw 17635 drsprs 18349 ipodrscl 18583 subgrcl 19149 pmtrfconj 19484 pgpprm 19611 slwprm 19627 efgsdmi 19750 efgsrel 19752 efgs1b 19754 efgsp1 19755 efgsres 19756 efgsfo 19757 efgredlema 19758 efgredlemf 19759 efgredlemd 19762 efgredlemc 19763 efgredlem 19765 efgrelexlemb 19768 efgcpbllemb 19773 rngabl 20152 srgcmn 20186 ringgrp 20235 irredcl 20424 subrngrcl 20551 sdrgrcl 20790 lmodgrp 20865 lssss 20934 phllvec 21647 obsrcl 21743 locfintop 23529 fclstop 24019 tmdmnd 24083 tgpgrp 24086 trgtgp 24176 tdrgtrg 24181 ust0 24228 ngpgrp 24612 elii1 24964 elii2 24965 icopnfcnv 24973 icopnfhmeo 24974 iccpnfhmeo 24976 xrhmeo 24977 oprpiece1res2 24983 phtpcer 25027 pcoval2 25049 pcoass 25057 clmlmod 25100 cphphl 25205 cphnlm 25206 cphsca 25213 bnnvc 25374 uc1pcl 26183 mon1pcl 26184 sinq12ge0 26550 cosq14ge0 26553 cosq34lt1 26569 cosord 26573 cos11 26575 recosf1o 26577 resinf1o 26578 efifo 26589 logrncn 26604 atanf 26923 atanneg 26950 efiatan 26955 atanlogaddlem 26956 atanlogadd 26957 atanlogsub 26959 efiatan2 26960 2efiatan 26961 tanatan 26962 areass 27002 dchrvmasumlem2 27542 dchrvmasumiflem1 27545 brbtwn2 28920 ax5seglem1 28943 ax5seglem2 28944 ax5seglem3 28946 ax5seglem5 28948 ax5seglem6 28949 ax5seglem9 28952 ax5seg 28953 axbtwnid 28954 axpaschlem 28955 axpasch 28956 axcontlem2 28980 axcontlem4 28982 axcontlem7 28985 pthistrl 29743 clwwlkbp 30004 sticl 32234 hstcl 32236 omndmnd 33081 slmdcmn 33211 orngring 33330 rrextnrg 34002 rrextdrg 34003 rossspw 34170 srossspw 34177 eulerpartlemd 34368 eulerpartlemf 34372 eulerpartlemgvv 34378 eulerpartlemgu 34379 eulerpartlemgh 34380 eulerpartlemgs2 34382 eulerpartlemn 34383 bnj564 34758 bnj1366 34843 bnj545 34909 bnj548 34911 bnj558 34916 bnj570 34919 bnj580 34927 bnj929 34950 bnj998 34971 bnj1006 34974 bnj1190 35022 bnj1523 35085 msrval 35543 mthmpps 35587 eqvrelrefrel 38599 atllat 39301 stoweidlem60 46075 fourierdlem111 46232 prproropf1o 47494 gpgedgvtx1 48020 gpg3nbgrvtxlem 48023 |
| Copyright terms: Public domain | W3C validator |