Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.74da | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 275. (Contributed by NM, 4-May-2007.) |
Ref | Expression |
---|---|
pm5.74da.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
pm5.74da | ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.74da.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | ex 415 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
3 | 2 | pm5.74d 275 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: cbvaldvaw 2045 sb4b 2499 sb4bOLD 2500 ralbidva 3196 ralbida 3230 vtocl2d 3557 vtocl2 3561 vtocl3 3563 spc3egv 3604 ralxpxfr2d 3639 elrab3t 3679 vtocl2dOLD 3931 csbie2df 4392 ordunisuc2 7559 dfom2 7582 pwfseqlem3 10082 lo1resb 14921 rlimresb 14922 o1resb 14923 fsumparts 15161 isprm3 16027 ramval 16344 islindf4 20982 cnntr 21883 fclsbas 22629 metcnp 23151 voliunlem3 24153 ellimc2 24475 limcflf 24479 mdegleb 24658 xrlimcnp 25546 dchrelbas3 25814 lmicom 26574 dmdbr5ati 30199 isarchi3 30816 islinds5 30932 cmpcref 31114 sscoid 33374 cdlemefrs29bpre0 37547 cdlemkid3N 38084 cdlemkid4 38085 hdmap1eulem 38973 hdmap1eulemOLDN 38974 jm2.25 39616 ntrneik2 40462 ntrneix2 40463 ntrneikb 40464 fourierdlem87 42498 |
Copyright terms: Public domain | W3C validator |