| 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 346 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) | |
| 4 | 1, 2, 3 | mp2 9 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: orimdi 931 nanbi 1500 rb-bijust 1749 sbnf 2312 sbnf2 2361 sb8mo 2601 raleqbii 3344 rmo5 3400 cbvrmo 3429 sstr2 3990 ss2ab 4062 sbcssg 4520 ssextss 5458 ssrel3 5796 relop 5861 dmcosseq 5987 dmcosseqOLD 5988 cotrgOLDOLD 6129 cnvsymOLDOLD 6134 intasym 6135 intirr 6138 codir 6140 qfto 6141 cnvpo 6307 dfpo2 6316 dffun2 6571 dffun2OLD 6572 dff14a 7290 porpss 7747 funcnvuni 7954 poxp 8153 infcllem 9527 ttrclss 9760 cp 9931 aceq2 10159 kmlem12 10202 kmlem15 10205 zfcndpow 10656 grothprim 10874 dfinfre 12249 infrenegsup 12251 xrinfmss2 13353 algcvgblem 16614 isprm2 16719 odulub 18452 oduglb 18454 isirred2 20421 isdomn2OLD 20712 isdomn3 20715 opprdomnb 20717 ntreq0 23085 ist0-3 23353 ist1-3 23357 ordthaus 23392 dfconn2 23427 iscusp2 24311 mdsymlem8 32429 mo5f 32508 iuninc 32573 suppss2f 32648 tosglblem 32964 prmidl0 33478 esumpfinvalf 34077 bnj110 34872 bnj92 34876 bnj539 34905 bnj540 34906 axrepprim 35702 axacprim 35707 dffr5 35754 dfso2 35755 elpotr 35782 bj-alcomexcom 36681 itg2addnclem2 37679 isdmn3 38081 sbcimi 38117 inxpss3 38315 trcoss2 38485 unitscyglem3 42198 eu6w 42686 moxfr 42703 ifpim123g 43513 elmapintrab 43589 undmrnresiss 43617 cnvssco 43619 snhesn 43799 psshepw 43801 frege77 43953 frege93 43969 frege116 43992 frege118 43994 frege131 44007 frege133 44009 ntrneikb 44107 ismnuprim 44313 onfrALTlem5 44562 onfrALTlem5VD 44905 dfac5prim 45007 setis 49217 |
| Copyright terms: Public domain | W3C validator |