![]() |
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 109 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | sylancom.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-ia2 106 ax-ia3 107 |
This theorem is referenced by: ordin 4265 fimacnvdisj 5263 fvimacnv 5487 ssct 6663 f1vrnfibi 6783 inl11 6900 ctssdc 6948 enomnilem 6958 djuen 7012 cauappcvgprlemlol 7397 cauappcvgprlemladdru 7406 cauappcvgprlemladdrl 7407 caucvgprlemlol 7420 caucvgprlemladdrl 7428 caucvgprprlemlol 7448 recgt1i 8560 avgle2 8859 xnn0le2is012 9536 ioodisj 9663 fzneuz 9768 fihashfn 10433 shftfvalg 10477 shftfval 10480 cvg1nlemres 10643 resqrexlem1arp 10663 maxabslemval 10866 xrmaxiflemval 10905 xrmaxadd 10916 xrminmax 10920 summodclem3 11035 fsumsplit 11062 mertenslemub 11189 demoivreALT 11324 zsupcllemstep 11480 gcdsupex 11488 gcdsupcl 11489 gcdneg 11512 bezoutlemsup 11537 eucalginv 11577 eucalg 11580 ctiunctlemfo 11789 iscnp4 12223 cnntr 12230 tx2cn 12275 xmetres2 12362 metres2 12364 limccnp2cntop 12596 isomninnlem 12906 |
Copyright terms: Public domain | W3C validator |