![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
3 | 2 | pm5.32d 450 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: rexbida 2472 reubida 2658 rmobida 2663 mpteq12f 4083 reuhypd 4471 funbrfv2b 5560 dffn5im 5561 eqfnfv2 5614 fndmin 5623 fniniseg 5636 rexsupp 5640 fmptco 5682 dff13 5768 riotabidva 5846 mpoeq123dva 5935 mpoeq3dva 5938 mpoxopovel 6241 qliftfun 6616 erovlem 6626 xpcomco 6825 elfi2 6970 ctssdccl 7109 ltexpi 7335 dfplpq2 7352 axprecex 7878 zrevaddcl 9301 qrevaddcl 9642 icoshft 9988 fznn 10086 shftdm 10826 2shfti 10835 sumeq2 11362 fsum3 11390 fsum2dlemstep 11437 prodeq2 11560 fprodseq 11586 gcdaddm 11979 grpidpropdg 12747 ismgmid 12750 mhmpropd 12811 issubm2 12818 eqgid 13038 iscrng2 13151 ringpropd 13170 crngpropd 13171 crngunit 13233 dvdsrpropdg 13269 issubrg3 13328 bastop2 13477 restopn2 13576 iscnp3 13596 lmbr2 13607 txlm 13672 ismet2 13747 xblpnfps 13791 xblpnf 13792 blininf 13817 blres 13827 elmopn2 13842 neibl 13884 metrest 13899 metcnp3 13904 metcnp 13905 metcnp2 13906 metcn 13907 txmetcn 13912 cnbl0 13927 cnblcld 13928 bl2ioo 13935 elcncf2 13954 cncfmet 13972 cnlimc 14034 |
Copyright terms: Public domain | W3C validator |