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 348 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) | |
4 | 1, 2, 3 | mp2 9 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 |
This theorem is referenced by: orimdi 924 nanbi 1484 rb-bijust 1741 sbnf2 2368 sb8mo 2680 cbvmow 2681 raleqbii 3231 rmo5 3432 cbvrmow 3442 cbvrmo 3446 ss2ab 4036 sbcssg 4459 ssextss 5337 relop 5714 dmcosseq 5837 cotrg 5964 cnvsym 5967 intasym 5968 intirr 5971 codir 5973 qfto 5974 cnvpo 6131 dff14a 7019 porpss 7442 funcnvuni 7625 poxp 7811 infcllem 8939 cp 9308 aceq2 9533 kmlem12 9575 kmlem15 9578 zfcndpow 10026 grothprim 10244 dfinfre 11610 infrenegsup 11612 xrinfmss2 12692 algcvgblem 15909 isprm2 16014 oduglb 17737 odulub 17739 isirred2 19380 isdomn2 20000 ntreq0 21613 ist0-3 21881 ist1-3 21885 ordthaus 21920 dfconn2 21955 iscusp2 22838 mdsymlem8 30114 mo5f 30180 iuninc 30240 suppss2f 30312 tosglblem 30583 esumpfinvalf 31234 bnj110 32029 bnj92 32033 bnj539 32062 bnj540 32063 axrepprim 32825 axacprim 32830 dffr5 32886 dfso2 32887 dfpo2 32888 elpotr 32923 bj-alcomexcom 33911 itg2addnclem2 34825 isdmn3 35233 sbcimi 35269 ssrel3 35437 inxpss3 35452 trcoss2 35604 moxfr 39167 isdomn3 39682 ifpim123g 39744 elmapintrab 39814 undmrnresiss 39842 cnvssco 39844 snhesn 40010 psshepw 40012 frege77 40164 frege93 40180 frege116 40203 frege118 40205 frege131 40218 frege133 40220 ntrneikb 40322 ismnuprim 40507 onfrALTlem5 40753 onfrALTlem5VD 41096 setis 44728 |
Copyright terms: Public domain | W3C validator |