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 447 | 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 2465 reubida 2651 rmobida 2656 mpteq12f 4069 reuhypd 4456 funbrfv2b 5541 dffn5im 5542 eqfnfv2 5594 fndmin 5603 fniniseg 5616 rexsupp 5620 fmptco 5662 dff13 5747 riotabidva 5825 mpoeq123dva 5914 mpoeq3dva 5917 mpoxopovel 6220 qliftfun 6595 erovlem 6605 xpcomco 6804 elfi2 6949 ctssdccl 7088 ltexpi 7299 dfplpq2 7316 axprecex 7842 zrevaddcl 9262 qrevaddcl 9603 icoshft 9947 fznn 10045 shftdm 10786 2shfti 10795 sumeq2 11322 fsum3 11350 fsum2dlemstep 11397 prodeq2 11520 fprodseq 11546 gcdaddm 11939 grpidpropdg 12628 ismgmid 12631 mhmpropd 12689 bastop2 12878 restopn2 12977 iscnp3 12997 lmbr2 13008 txlm 13073 ismet2 13148 xblpnfps 13192 xblpnf 13193 blininf 13218 blres 13228 elmopn2 13243 neibl 13285 metrest 13300 metcnp3 13305 metcnp 13306 metcnp2 13307 metcn 13308 txmetcn 13313 cnbl0 13328 cnblcld 13329 bl2ioo 13336 elcncf2 13355 cncfmet 13373 cnlimc 13435 |
Copyright terms: Public domain | W3C validator |