![]() |
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 301 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl112anc.5 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 2, 5, 6 | syl3anc 1181 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: fvun1 5405 caseinl 6862 reapmul1 8169 recrecap 8273 rec11rap 8275 divdivdivap 8277 dmdcanap 8286 ddcanap 8290 rerecclap 8294 div2negap 8299 divap1d 8365 divmulapd 8376 apdivmuld 8377 divmulap2d 8388 divmulap3d 8389 divassapd 8390 div12apd 8391 div23apd 8392 divdirapd 8393 divsubdirapd 8394 div11apd 8395 ltmul12a 8418 ltdiv1 8426 ltrec 8441 lt2msq1 8443 lediv2 8449 lediv23 8451 recp1lt1 8457 qapne 9223 xadd4d 9451 xleaddadd 9453 modqge0 9888 modqlt 9889 modqid 9905 expgt1 10124 nnlesq 10189 expnbnd 10208 facubnd 10284 resqrexlemover 10574 mulcn2 10871 cvgratnnlemnexp 11083 cvgratnnlemmn 11084 eftlub 11145 eflegeo 11157 sin01bnd 11213 cos01bnd 11214 eirraplem 11229 bezoutlemnewy 11428 bezoutlemstep 11429 mulgcd 11448 mulgcddvds 11519 prmind2 11545 oddpwdclemxy 11590 oddpwdclemodd 11593 qnumgt0 11619 xblm 12219 |
Copyright terms: Public domain | W3C validator |