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 195 |
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 196 |
This theorem is referenced by: orimdi 888 nanbi 1446 rb-bijust 1665 nfbii 1770 nfbiiOLD 1824 sbnf2 2427 sb8mo 2492 cbvmo 2494 raleqbii 2973 rmo5 3139 cbvrmo 3146 ss2ab 3633 sbcssg 4035 trint 4696 ssextss 4849 relop 5194 dmcosseq 5308 cotrg 5426 issref 5428 cnvsym 5429 intasym 5430 intirr 5433 codir 5435 qfto 5436 cnvpo 5590 dff14a 6427 porpss 6839 funcnvuni 7012 poxp 7176 infcllem 8276 cp 8637 aceq2 8825 kmlem12 8866 kmlem15 8869 zfcndpow 9317 grothprim 9535 dfinfre 10881 infrenegsup 10883 xrinfmss2 12013 algcvgblem 15128 isprm2 15233 oduglb 16962 odulub 16964 isirred2 18524 isdomn2 19120 ntreq0 20691 ist0-3 20959 ist1-3 20963 ordthaus 20998 dfcon2 21032 iscusp2 21916 mdsymlem8 28653 mo5f 28708 iuninc 28761 suppss2f 28819 tosglblem 29000 esumpfinvalf 29465 bnj110 30182 bnj92 30186 bnj539 30215 bnj540 30216 axrepprim 30833 axacprim 30838 dffr5 30896 dfso2 30897 dfpo2 30898 elpotr 30930 gtinfOLD 31484 bj-alcomexcom 31857 itg2addnclem2 32632 isdmn3 33043 sbcimi 33082 moxfr 36273 isdomn3 36801 ifpim123g 36864 elmapintrab 36901 undmrnresiss 36929 cnvssco 36931 snhesn 37100 psshepw 37102 frege77 37254 frege93 37270 frege116 37293 frege118 37295 frege131 37308 frege133 37310 ntrneikb 37412 conss34OLD 37667 onfrALTlem5 37778 onfrALTlem5VD 38143 frgr2wwlkeqm 41496 |
Copyright terms: Public domain | W3C validator |