Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad3antrrr | GIF version |
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad3antrrr | ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | adantr 261 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad2antrr 457 | 1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
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 is referenced by: ad4antr 463 phplem4on 6329 ltaddpr 6695 ltexprlemrl 6708 addcanprleml 6712 addcanprlemu 6713 aptiprleml 6737 aptiprlemu 6738 cauappcvgprlemdisj 6749 cauappcvgprlemladdrl 6755 caucvgprlemloc 6773 caucvgprlemladdrl 6776 caucvgprprlemopl 6795 caucvgprprlemloc 6801 caucvgprprlemexbt 6804 caucvgsrlemoffres 6884 axcaucvglemcau 6972 axcaucvglemres 6973 apreim 7594 apsym 7597 apcotr 7598 apadd1 7599 apneg 7602 mulext1 7603 mulge0 7610 apti 7613 qapne 8574 qtri3or 9098 qbtwnzlemstep 9103 rebtwn2zlemstep 9107 cvg1nlemres 9584 resqrexlemoverl 9619 resqrexlemglsq 9620 resqrexlemga 9621 climrecvg1n 9867 serif0 9871 |
Copyright terms: Public domain | W3C validator |