Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imbi12i | Structured version Visualization version GIF version |
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.) |
Ref | Expression |
---|---|
imbi12i.1 | ⊢ (𝜑 ↔ 𝜓) |
imbi12i.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
imbi12i | ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | imbi12i.2 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
3 | imbi12 350 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) | |
4 | 1, 2, 3 | mp2 9 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: orimdi 931 nanbi 1496 rb-bijust 1757 sbnf2 2359 sb8mo 2602 cbvmowOLD 2605 raleqbii 3161 rmo5 3356 cbvrmowOLD 3368 cbvrmo 3372 ss2ab 3990 sbcssg 4452 ssextss 5355 relop 5737 dmcosseq 5860 cotrg 5994 cnvsym 5997 intasym 5998 intirr 6001 codir 6003 qfto 6004 cnvpo 6168 dfpo2 6177 dff14a 7104 porpss 7537 funcnvuni 7731 poxp 7919 infcllem 9133 cp 9537 aceq2 9763 kmlem12 9805 kmlem15 9808 zfcndpow 10260 grothprim 10478 dfinfre 11843 infrenegsup 11845 xrinfmss2 12931 algcvgblem 16167 isprm2 16272 odulub 17946 oduglb 17948 isirred2 19752 isdomn2 20370 ntreq0 22006 ist0-3 22274 ist1-3 22278 ordthaus 22313 dfconn2 22348 iscusp2 23231 mdsymlem8 30523 mo5f 30588 iuninc 30651 suppss2f 30725 tosglblem 31003 prmidl0 31372 esumpfinvalf 31788 bnj110 32582 bnj92 32586 bnj539 32615 bnj540 32616 axrepprim 33387 axacprim 33392 dffr5 33471 dfso2 33472 elpotr 33507 ttrclss 33550 bj-alcomexcom 34633 itg2addnclem2 35603 isdmn3 36006 sbcimi 36042 ssrel3 36208 inxpss3 36223 trcoss2 36376 moxfr 40265 isdomn3 40780 ifpim123g 40840 elmapintrab 40908 undmrnresiss 40936 cnvssco 40938 snhesn 41119 psshepw 41121 frege77 41273 frege93 41289 frege116 41312 frege118 41314 frege131 41327 frege133 41329 ntrneikb 41429 ismnuprim 41633 onfrALTlem5 41883 onfrALTlem5VD 42226 setis 46120 |
Copyright terms: Public domain | W3C validator |