![]() |
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 335 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) | |
4 | 1, 2, 3 | mp2 9 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 |
This theorem is referenced by: orimdi 910 nanbi 1494 rb-bijust 1714 nfbiiOLD 1876 sbnf2 2467 sb8mo 2533 cbvmo 2535 raleqbii 3019 rmo5 3192 cbvrmo 3200 ss2ab 3703 sbcssg 4118 trint 4801 ssextss 4952 relop 5305 dmcosseq 5419 cotrg 5542 issref 5544 cnvsym 5545 intasym 5546 intirr 5549 codir 5551 qfto 5552 cnvpo 5711 dff14a 6567 porpss 6983 funcnvuni 7161 poxp 7334 infcllem 8434 cp 8792 aceq2 8980 kmlem12 9021 kmlem15 9024 zfcndpow 9476 grothprim 9694 dfinfre 11042 infrenegsup 11044 xrinfmss2 12179 algcvgblem 15337 isprm2 15442 oduglb 17186 odulub 17188 isirred2 18747 isdomn2 19347 ntreq0 20929 ist0-3 21197 ist1-3 21201 ordthaus 21236 dfconn2 21270 iscusp2 22153 mdsymlem8 29397 mo5f 29452 iuninc 29505 suppss2f 29567 tosglblem 29797 esumpfinvalf 30266 bnj110 31054 bnj92 31058 bnj539 31087 bnj540 31088 axrepprim 31705 axacprim 31710 dffr5 31769 dfso2 31770 dfpo2 31771 elpotr 31810 gtinfOLD 32439 bj-alcomexcom 32795 itg2addnclem2 33592 isdmn3 34003 sbcimi 34042 ssrel3 34208 inxpss3 34225 trcoss2 34374 moxfr 37572 isdomn3 38099 ifpim123g 38162 elmapintrab 38199 undmrnresiss 38227 cnvssco 38229 snhesn 38397 psshepw 38399 frege77 38551 frege93 38567 frege116 38590 frege118 38592 frege131 38605 frege133 38607 ntrneikb 38709 conss34OLD 38963 onfrALTlem5 39074 onfrALTlem5VD 39435 setis 42769 |
Copyright terms: Public domain | W3C validator |