Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.32d | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.) |
Ref | Expression |
---|---|
pm5.32d.1 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.32d | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | pm5.32 666 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) | |
3 | 1, 2 | sylib 207 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: pm5.32rd 670 pm5.32da 671 anbi2d 736 raltpd 4258 cores 5555 isoini 6488 mpt2eq123 6612 ordpwsuc 6907 rdglim2 7415 fzind 11351 btwnz 11355 elfzm11 12280 isprm2 15233 isprm3 15234 modprminv 15342 modprminveq 15343 isrim 18556 elimifd 28746 funcnvmptOLD 28850 xrecex 28959 ordtconlem1 29298 indpi1 29411 dfres3 30902 dfrdg4 31228 ee7.2aOLD 31630 wl-ax11-lem8 32548 expdioph 36608 pm14.122b 37646 rexbidar 37671 mapsnend 38386 isrngim 41694 |
Copyright terms: Public domain | W3C validator |