![]() |
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 502. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpa 502 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | 3impa 1101 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 |
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 1074 |
This theorem is referenced by: nn0addge1 11527 nn0addge2 11528 nn0sub2 11626 eluzp1p1 11901 uznn0sub 11908 uzinfi 11957 iocssre 12442 icossre 12443 iccssre 12444 lincmb01cmp 12504 iccf1o 12505 fzosplitprm1 12768 subfzo0 12780 modfzo0difsn 12932 hashprb 13373 swrd0fv 13635 eflt 15042 fldivndvdslt 15336 prmdiv 15688 hashgcdlem 15691 vfermltl 15704 coprimeprodsq 15711 pythagtrip 15737 difsqpwdvds 15789 cshwshashlem2 16001 odinf 18176 odcl2 18178 slesolex 20686 tgtop11 20984 restntr 21184 hauscmplem 21407 icchmeo 22937 pi1xfr 23051 sinq12gt0 24454 tanord1 24478 gausslemma2dlem1a 25285 axsegconlem6 25997 lfuhgr1v0e 26341 crctcshwlkn0lem6 26914 crctcshwlkn0lem7 26915 clwlkclwwlkf1lem2 27124 s2elclwwlknon2 27248 eucrctshift 27391 eucrct2eupth 27393 nv1 27835 lnolin 27914 br8d 29725 ballotlemfc0 30859 ballotlemfcc 30860 ballotlemrv2 30888 br8 31949 br6 31950 br4 31951 ismtyima 33911 ismtybndlem 33914 ghomlinOLD 33996 ghomidOLD 33997 cvrcmp2 35070 atcvrj2 35218 1cvratex 35258 lplnric 35337 lplnri1 35338 lnatexN 35564 ltrnateq 35967 ltrnatneq 35968 cdleme46f2g2 36279 cdleme46f2g1 36280 dibelval1st 36936 dibelval2nd 36939 dicelval1sta 36974 hlhilphllem 37749 jm2.17b 38026 bi123impia 39193 sineq0ALT 39668 eliccre 40227 ioomidp 40239 smfinflem 41525 iccpartiltu 41864 pfxpfx 41921 repswpfx 41942 goldbachthlem1 41963 evengpop3 42192 rnghmresel 42470 rhmresel 42516 |
Copyright terms: Public domain | W3C validator |