![]() |
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 300 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl112anc.5 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 2, 5, 6 | syl3anc 1170 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: fvun1 5265 reapmul1 7751 recrecap 7853 rec11rap 7855 divdivdivap 7857 dmdcanap 7866 ddcanap 7870 rerecclap 7874 div2negap 7879 divap1d 7944 divmulapd 7955 divmulap2d 7966 divmulap3d 7967 divassapd 7968 div12apd 7969 div23apd 7970 divdirapd 7971 divsubdirapd 7972 div11apd 7973 ltmul12a 7994 ltdiv1 8002 ltrec 8017 lt2msq1 8019 lediv2 8025 lediv23 8027 recp1lt1 8033 qapne 8794 modqge0 9403 modqlt 9404 modqid 9420 expgt1 9600 nnlesq 9664 expnbnd 9682 facubnd 9758 resqrexlemover 10023 mulcn2 10278 bezoutlemnewy 10518 bezoutlemstep 10519 mulgcd 10538 mulgcddvds 10609 prmind2 10635 oddpwdclemxy 10680 oddpwdclemodd 10683 |
Copyright terms: Public domain | W3C validator |