![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biimp3a | Structured version Visualization version GIF version |
Description: Infer implication from a logical equivalence. Similar to biimpa 477. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpa 477 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | 3impa 1103 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: nn0addge1 11793 nn0addge2 11794 nn0sub2 11893 eluzp1p1 12119 uznn0sub 12126 uzinfi 12177 iocssre 12666 icossre 12667 iccssre 12668 lincmb01cmp 12731 iccf1o 12732 fzosplitprm1 12997 subfzo0 13009 modfzo0difsn 13161 hashprb 13606 pfxpfx 13906 repswpfx 13983 eflt 15303 fldivndvdslt 15598 prmdiv 15951 hashgcdlem 15954 vfermltl 15967 coprimeprodsq 15974 pythagtrip 16000 difsqpwdvds 16052 cshwshashlem2 16259 odinf 18420 odcl2 18422 slesolex 20975 tgtop11 21274 restntr 21474 hauscmplem 21698 icchmeo 23228 pi1xfr 23342 sinq12gt0 24776 tanord1 24802 gausslemma2dlem1a 25623 axsegconlem6 26391 lfuhgr1v0e 26719 crctcshwlkn0lem6 27275 crctcshwlkn0lem7 27276 clwlkclwwlkf1lem2 27465 s2elclwwlknon2 27565 eucrctshift 27704 eucrct2eupth 27706 nv1 28135 lnolin 28214 br8d 30043 ballotlemfc0 31359 ballotlemfcc 31360 ballotlemrv2 31388 fisshasheq 31958 br8 32594 br6 32595 br4 32596 ismtyima 34626 ismtybndlem 34629 ghomlinOLD 34711 ghomidOLD 34712 cvrcmp2 35964 atcvrj2 36113 1cvratex 36153 lplnric 36232 lplnri1 36233 lnatexN 36459 ltrnateq 36861 ltrnatneq 36862 cdleme46f2g2 37173 cdleme46f2g1 37174 dibelval1st 37829 dibelval2nd 37832 dicelval1sta 37867 hlhilphllem 38639 jm2.17b 39056 bi123impia 40375 sineq0ALT 40823 eliccre 41336 ioomidp 41345 smfinflem 42647 iccpartiltu 43078 goldbachthlem1 43203 evengpop3 43459 rnghmresel 43727 rhmresel 43773 |
Copyright terms: Public domain | W3C validator |