|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > bibi2d | Structured version Visualization version GIF version | ||
| Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) | 
| Ref | Expression | 
|---|---|
| imbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | 
| Ref | Expression | 
|---|---|
| bibi2d | ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | imbid.1 | . . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | pm5.74i 271 | . . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) | 
| 3 | 2 | bibi2i 337 | . . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒))) | 
| 4 | pm5.74 270 | . . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓))) | |
| 5 | pm5.74 270 | . . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒))) | |
| 6 | 3, 4, 5 | 3bitr4i 303 | . 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒))) | 
| 7 | 6 | pm5.74ri 272 | 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: bibi1d 343 bibi12d 345 biantr 805 eujust 2570 eujustALT 2571 euf 2575 reu6i 3733 sbc2or 3796 axrep1 5279 axreplem 5280 zfrepclf 5290 axsepg 5296 zfauscl 5297 notzfaus 5362 copsexgw 5494 copsexg 5495 euotd 5517 cnveq0 6216 iotavalOLD 6534 iota5 6543 eufnfv 7250 isoeq1 7338 isoeq3 7340 isores2 7354 isores3 7356 isotr 7357 isoini2 7360 riota5f 7417 caovordg 7641 caovord 7645 dfoprab4f 8082 seqomlem2 8492 xpf1o 9180 aceq0 10159 dfac5 10170 zfac 10501 zfcndrep 10655 zfcndac 10660 ltasr 11141 axpre-ltadd 11208 absmod0 15343 absz 15351 smuval2 16520 prmdvdsexp 16753 isacs2 17697 isacs1i 17701 mreacs 17702 abvfval 20812 abvpropd 20837 isclo2 23097 t0sep 23333 kqt0lem 23745 r0sep 23757 iccpnfcnv 24976 rolle 26029 2sqreultlem 27492 2sqreunnltlem 27495 tgjustr 28483 wlkeq 29653 eigre 31855 fgreu 32683 fcnvgreu 32684 gsumhashmul 33065 xrge0iifcnv 33933 axsepg2 35097 axsepg2ALT 35098 cvmlift2lem13 35321 iota5f 35725 nn0prpwlem 36324 nn0prpw 36325 bj-zfauscl 36926 wl-eudf 37574 ismndo2 37882 islaut 40086 ispautN 40102 mrefg2 42723 zindbi 42963 jm2.19lem3 43008 oaordnr 43314 omnord1 43323 oenord1 43334 alephiso2 43576 ntrneiel2 44104 ntrneik4 44119 iotavalb 44454 eusnsn 47043 aiota0def 47113 fargshiftfo 47434 isuspgrimlem 47879 line2x 48680 eufsnlem 48755 thincciso 49127 thinccisod 49128 termcarweu 49186 | 
| Copyright terms: Public domain | W3C validator |