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 304 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl112anc.5 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 2, 5, 6 | syl3anc 1227 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: fvun1 5546 caseinl 7047 caseinr 7048 reapmul1 8484 recrecap 8596 rec11rap 8598 divdivdivap 8600 dmdcanap 8609 ddcanap 8613 rerecclap 8617 div2negap 8622 divap1d 8688 divmulapd 8699 apdivmuld 8700 divmulap2d 8711 divmulap3d 8712 divassapd 8713 div12apd 8714 div23apd 8715 divdirapd 8716 divsubdirapd 8717 div11apd 8718 ltmul12a 8746 ltdiv1 8754 ltrec 8769 lt2msq1 8771 lediv2 8777 lediv23 8779 recp1lt1 8785 qapne 9568 xadd4d 9812 xleaddadd 9814 modqge0 10257 modqlt 10258 modqid 10274 expgt1 10483 nnlesq 10548 expnbnd 10567 facubnd 10647 resqrexlemover 10938 mulcn2 11239 cvgratnnlemnexp 11451 cvgratnnlemmn 11452 eftlub 11617 eflegeo 11628 sin01bnd 11684 cos01bnd 11685 eirraplem 11703 bezoutlemnewy 11914 bezoutlemstep 11915 mulgcd 11934 mulgcddvds 12005 prmind2 12031 oddpwdclemxy 12080 oddpwdclemodd 12083 qnumgt0 12109 pcpremul 12204 fldivp1 12257 pcfaclem 12258 qexpz 12261 prmpwdvds 12264 pockthg 12266 txdis 12824 txdis1cn 12825 xblm 12964 reeff1oleme 13240 tangtx 13306 cosordlem 13317 logdivlti 13349 apcxp2 13405 apdifflemr 13767 |
Copyright terms: Public domain | W3C validator |