![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylancom | GIF version |
Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.) |
Ref | Expression |
---|---|
sylancom.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
sylancom.2 | ⊢ ((𝜒 ∧ 𝜓) → 𝜃) |
Ref | Expression |
---|---|
sylancom | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancom.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | simpr 108 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | sylancom.2 | . 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃) | |
4 | 1, 2, 3 | syl2anc 403 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: ordin 4175 fimacnvdisj 5142 fvimacnv 5358 ssct 6463 f1vrnfibi 6578 enomnilem 6698 cauappcvgprlemlol 7108 cauappcvgprlemladdru 7117 cauappcvgprlemladdrl 7118 caucvgprlemlol 7131 caucvgprlemladdrl 7139 caucvgprprlemlol 7159 recgt1i 8252 avgle2 8548 ioodisj 9304 fzneuz 9407 fihashfn 10042 shftfvalg 10079 shftfval 10082 cvg1nlemres 10244 resqrexlem1arp 10264 maxabslemval 10467 zsupcllemstep 10720 gcdsupex 10728 gcdsupcl 10729 gcdneg 10752 bezoutlemsup 10777 eucalginv 10817 eucialg 10820 |
Copyright terms: Public domain | W3C validator |