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 290 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl112anc.5 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 2, 5, 6 | syl3anc 1135 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: fvun1 5239 reapmul1 7586 recrecap 7685 rec11rap 7687 divdivdivap 7689 dmdcanap 7698 ddcanap 7702 rerecclap 7706 div2negap 7711 divap1d 7776 divmulapd 7787 divmulap2d 7798 divmulap3d 7799 divassapd 7800 div12apd 7801 div23apd 7802 divdirapd 7803 divsubdirapd 7804 div11apd 7805 ltmul12a 7826 ltdiv1 7834 ltrec 7849 lt2msq1 7851 lediv2 7857 lediv23 7859 recp1lt1 7865 qapne 8574 modqge0 9174 modqlt 9175 expgt1 9293 nnlesq 9356 expnbnd 9372 resqrexlemover 9608 mulcn2 9833 |
Copyright terms: Public domain | W3C validator |