Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpancom | GIF version |
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpancom.1 | ⊢ (𝜓 → 𝜑) |
mpancom.2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
mpancom | ⊢ (𝜓 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpancom.1 | . 2 ⊢ (𝜓 → 𝜑) | |
2 | id 19 | . 2 ⊢ (𝜓 → 𝜓) | |
3 | mpancom.2 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
4 | 1, 2, 3 | syl2anc 408 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mpan 420 spesbc 2966 onsucelsucr 4394 sucunielr 4396 ordsuc 4448 peano2b 4498 xpiindim 4646 fvelrnb 5437 fliftcnv 5664 riotaprop 5721 unielxp 6040 dmtpos 6121 tpossym 6141 ercnv 6418 cnvct 6671 php5dom 6725 3xpfi 6787 recrecnq 7170 1idpr 7368 eqlei2 7826 lem1 8573 eluzfz1 9779 fzpred 9818 uznfz 9851 fz0fzdiffz0 9875 fzctr 9878 flid 10025 flqeqceilz 10059 faclbnd3 10457 bcn1 10472 isfinite4im 10507 leabs 10814 gcd0id 11594 lcmgcdlem 11685 dvdsnprmd 11733 eltpsg 12134 tg1 12155 cldval 12195 cldss 12201 cldopn 12203 psmetdmdm 12420 dvef 12783 bj-nn0suc0 13075 |
Copyright terms: Public domain | W3C validator |