Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.32da | GIF version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.) |
Ref | Expression |
---|---|
pm5.32da.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
pm5.32da | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32da.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
3 | 2 | pm5.32d 445 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: rexbida 2409 reubida 2589 rmobida 2594 mpteq12f 3978 reuhypd 4362 funbrfv2b 5434 dffn5im 5435 eqfnfv2 5487 fndmin 5495 fniniseg 5508 rexsupp 5512 fmptco 5554 dff13 5637 riotabidva 5714 mpoeq123dva 5800 mpoeq3dva 5803 mpoxopovel 6106 qliftfun 6479 erovlem 6489 xpcomco 6688 elfi2 6828 ctssdccl 6964 ltexpi 7113 dfplpq2 7130 axprecex 7656 zrevaddcl 9072 qrevaddcl 9404 icoshft 9741 fznn 9837 shftdm 10562 2shfti 10571 sumeq2 11096 fsum3 11124 fsum2dlemstep 11171 gcdaddm 11599 bastop2 12180 restopn2 12279 iscnp3 12299 lmbr2 12310 txlm 12375 ismet2 12450 xblpnfps 12494 xblpnf 12495 blininf 12520 blres 12530 elmopn2 12545 neibl 12587 metrest 12602 metcnp3 12607 metcnp 12608 metcnp2 12609 metcn 12610 txmetcn 12615 cnbl0 12630 cnblcld 12631 bl2ioo 12638 elcncf2 12657 cncfmet 12675 cnlimc 12737 |
Copyright terms: Public domain | W3C validator |