![]() |
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 338 | . . 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 205 |
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 206 |
This theorem is referenced by: bibi1d 344 bibi12d 346 biantr 805 eujust 2570 eujustALT 2571 euf 2575 reu6i 3687 sbc2or 3749 axrep1 5244 axreplem 5245 zfrepclf 5252 axsepg 5258 zfauscl 5259 notzfaus 5319 copsexgw 5448 copsexg 5449 euotd 5471 cnveq0 6150 iotavalOLD 6471 iota5 6480 eufnfv 7180 isoeq1 7263 isoeq3 7265 isores2 7279 isores3 7281 isotr 7282 isoini2 7285 riota5f 7343 caovordg 7562 caovord 7566 dfoprab4f 7989 seqomlem2 8398 xpf1o 9084 aceq0 10055 dfac5 10065 zfac 10397 zfcndrep 10551 zfcndac 10556 ltasr 11037 axpre-ltadd 11104 absmod0 15189 absz 15197 smuval2 16363 prmdvdsexp 16592 isacs2 17534 isacs1i 17538 mreacs 17539 abvfval 20280 abvpropd 20304 isclo2 22442 t0sep 22678 kqt0lem 23090 r0sep 23102 iccpnfcnv 24310 rolle 25357 2sqreultlem 26798 2sqreunnltlem 26801 tgjustr 27419 wlkeq 28585 eigre 30780 fgreu 31591 fcnvgreu 31592 gsumhashmul 31901 xrge0iifcnv 32517 cvmlift2lem13 33912 iota5f 34298 nn0prpwlem 34797 nn0prpw 34798 bj-zfauscl 35397 wl-eudf 36030 ismndo2 36336 islaut 38549 ispautN 38565 mrefg2 41033 zindbi 41273 jm2.19lem3 41318 oaordnr 41633 omnord1 41642 oenord1 41653 alephiso2 41837 ntrneiel2 42365 ntrneik4 42380 iotavalb 42717 eusnsn 45267 aiota0def 45335 fargshiftfo 45641 line2x 46847 eufsnlem 46914 thincciso 47076 |
Copyright terms: Public domain | W3C validator |