![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl13anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
syl13anc.5 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) |
Ref | Expression |
---|---|
syl13anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | sylXanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 2, 3, 4 | 3jca 1177 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
6 | syl13anc.5 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 5, 6 | syl2anc 411 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
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 df-3an 980 |
This theorem is referenced by: syl23anc 1245 syl33anc 1253 caovassd 6033 caovcand 6036 caovordid 6040 caovordd 6042 caovdid 6049 caovdird 6052 swoer 6562 swoord1 6563 swoord2 6564 fimax2gtrilemstep 6899 iunfidisj 6944 ssfii 6972 suplub2ti 6999 prarloclem3 7495 fzosubel3 10195 seq3split 10478 seq3caopr 10482 zsumdc 11391 fsumiun 11484 divalglemex 11926 pcgcd1 12326 strle1g 12564 mnd32g 12827 mnd12g 12828 mnd4g 12829 ismndd 12837 mndinvmod 12845 grpasscan2 12933 grpidrcan 12934 grpidlcan 12935 grpinvinv 12936 grplmulf1o 12943 grpinvssd 12946 grpinvadd 12947 grpsubrcan 12950 grpsubadd 12957 grpaddsubass 12959 grppncan 12960 grpsubsub4 12962 grppnpcan2 12963 grpnpncan 12964 grpnpncan0 12965 grpnnncan2 12966 dfgrp3mlem 12967 dfgrp3m 12968 grplactcnv 12971 mhmmnd 12979 mulgaddcomlem 13004 mulgaddcom 13005 mulgnn0dir 13011 mulgdirlem 13012 mulgneg2 13015 mulgnnass 13016 mulgnn0ass 13017 mulgass 13018 mulgmodid 13020 nsgconj 13064 isnsg3 13065 nmzsubg 13068 ssnmz 13069 eqger 13081 eqgcpbl 13085 abl32 13108 abladdsub4 13115 abladdsub 13116 ablpncan2 13117 ablsubsub 13119 srgass 13152 srgmulgass 13170 srgpcomp 13171 srgpcompp 13172 srgpcomppsc 13173 ringass 13197 ringadd2 13208 rngo2times 13209 ringcom 13212 ringlz 13220 ringrz 13221 ringnegl 13226 rngnegr 13227 ringmneg1 13228 ringmneg2 13229 ringsubdi 13231 rngsubdir 13232 mulgass2 13233 opprring 13247 mulgass3 13252 dvdsrtr 13268 dvdsrmul1 13269 unitgrp 13283 dvrass 13306 dvrcan1 13307 dvrcan3 13308 dvrdir 13310 rdivmuldivd 13311 lringuplu 13335 aprcotr 13341 subrginv 13363 psmetsym 13765 psmettri 13766 psmetge0 13767 psmetres2 13769 xmetge0 13801 xmetsym 13804 xmettri 13808 metrtri 13813 xmetres2 13815 bldisj 13837 xblss2ps 13840 xblss2 13841 xmeter 13872 xmetxp 13943 |
Copyright terms: Public domain | W3C validator |