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 446 | 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 2452 reubida 2638 rmobida 2643 mpteq12f 4044 reuhypd 4431 funbrfv2b 5513 dffn5im 5514 eqfnfv2 5566 fndmin 5574 fniniseg 5587 rexsupp 5591 fmptco 5633 dff13 5718 riotabidva 5796 mpoeq123dva 5882 mpoeq3dva 5885 mpoxopovel 6188 qliftfun 6562 erovlem 6572 xpcomco 6771 elfi2 6916 ctssdccl 7055 ltexpi 7257 dfplpq2 7274 axprecex 7800 zrevaddcl 9217 qrevaddcl 9553 icoshft 9894 fznn 9991 shftdm 10722 2shfti 10731 sumeq2 11256 fsum3 11284 fsum2dlemstep 11331 prodeq2 11454 fprodseq 11480 gcdaddm 11868 bastop2 12495 restopn2 12594 iscnp3 12614 lmbr2 12625 txlm 12690 ismet2 12765 xblpnfps 12809 xblpnf 12810 blininf 12835 blres 12845 elmopn2 12860 neibl 12902 metrest 12917 metcnp3 12922 metcnp 12923 metcnp2 12924 metcn 12925 txmetcn 12930 cnbl0 12945 cnblcld 12946 bl2ioo 12953 elcncf2 12972 cncfmet 12990 cnlimc 13052 |
Copyright terms: Public domain | W3C validator |