![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl112anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
syl112anc.5 | ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) |
Ref | Expression |
---|---|
syl112anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | sylXanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 3, 4 | jca 306 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl112anc.5 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 2, 5, 6 | syl3anc 1249 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
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 982 |
This theorem is referenced by: fvun1 5603 caseinl 7120 caseinr 7121 reapmul1 8582 recrecap 8696 rec11rap 8698 divdivdivap 8700 dmdcanap 8709 ddcanap 8713 rerecclap 8717 div2negap 8722 divap1d 8788 divmulapd 8799 apdivmuld 8800 divmulap2d 8811 divmulap3d 8812 divassapd 8813 div12apd 8814 div23apd 8815 divdirapd 8816 divsubdirapd 8817 div11apd 8818 ltmul12a 8847 ltdiv1 8855 ltrec 8870 lt2msq1 8872 lediv2 8878 lediv23 8880 recp1lt1 8886 qapne 9669 xadd4d 9915 xleaddadd 9917 modqge0 10363 modqlt 10364 modqid 10380 expgt1 10589 nnlesq 10655 expnbnd 10675 facubnd 10757 resqrexlemover 11051 mulcn2 11352 cvgratnnlemnexp 11564 cvgratnnlemmn 11565 eftlub 11730 eflegeo 11741 sin01bnd 11797 cos01bnd 11798 eirraplem 11816 bezoutlemnewy 12029 bezoutlemstep 12030 mulgcd 12049 mulgcddvds 12126 prmind2 12152 oddpwdclemxy 12201 oddpwdclemodd 12204 qnumgt0 12230 pcpremul 12325 fldivp1 12380 pcfaclem 12381 qexpz 12384 prmpwdvds 12387 pockthg 12389 4sqlem10 12419 4sqlem12 12434 4sqlem16 12438 4sqlem17 12439 ablsub4 13252 txdis 14234 txdis1cn 14235 xblm 14374 reeff1oleme 14650 tangtx 14716 cosordlem 14727 logdivlti 14759 apcxp2 14815 lgsdilem 14886 lgseisenlem1 14908 lgseisenlem2 14909 2sqlem3 14922 2sqlem8 14928 apdifflemr 15254 |
Copyright terms: Public domain | W3C validator |