| 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 273. (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 412 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
| 3 | 2 | pm5.74d 273 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 df-an 396 |
| This theorem is referenced by: cbvaldvaw 2037 sb4b 2480 ralbidva 3176 cbvraldva 3239 ralbidaOLD 3271 vtocl2d 3562 vtocl2 3566 vtocl3 3567 spc3egv 3603 ralxpxfr2d 3646 elabd2 3670 elrab3t 3691 csbie2df 4443 ordunisuc2 7865 dfom2 7889 pwfseqlem3 10700 lo1resb 15600 rlimresb 15601 o1resb 15602 fsumparts 15842 isprm3 16720 ramval 17046 islindf4 21858 cnntr 23283 fclsbas 24029 metcnp 24554 voliunlem3 25587 ellimc2 25912 limcflf 25916 mdegleb 26103 xrlimcnp 27011 dchrelbas3 27282 lmicom 28796 dmdbr5ati 32441 isarchi3 33194 islinds5 33395 cmpcref 33849 sscoid 35914 bj-equsalvwd 36781 cdlemefrs29bpre0 40398 cdlemkid3N 40935 cdlemkid4 40936 hdmap1eulem 41824 hdmap1eulemOLDN 41825 jm2.25 43011 ntrneik2 44105 ntrneix2 44106 ntrneikb 44107 fourierdlem87 46208 |
| Copyright terms: Public domain | W3C validator |