![]() |
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 406 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: mpan 418 spesbc 2946 onsucelsucr 4362 sucunielr 4364 ordsuc 4416 peano2b 4466 xpiindim 4614 fvelrnb 5401 fliftcnv 5628 riotaprop 5685 unielxp 6002 dmtpos 6083 tpossym 6103 ercnv 6380 cnvct 6633 php5dom 6686 3xpfi 6748 recrecnq 7103 1idpr 7301 eqlei2 7729 lem1 8463 eluzfz1 9652 fzpred 9691 uznfz 9724 fz0fzdiffz0 9748 fzctr 9751 flid 9898 flqeqceilz 9932 faclbnd3 10330 bcn1 10345 isfinite4im 10380 leabs 10686 gcd0id 11462 lcmgcdlem 11551 dvdsnprmd 11599 eltpsg 11989 tg1 12010 cldval 12050 cldss 12056 cldopn 12058 psmetdmdm 12252 bj-nn0suc0 12733 |
Copyright terms: Public domain | W3C validator |