![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad3antlr | GIF version |
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad3antlr | ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ad2antlr 489 | . 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓) |
3 | 2 | adantr 276 | 1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: ad4antlr 495 nntr2 6503 phpm 6864 phplem4on 6866 fidifsnen 6869 fisbth 6882 fin0 6884 fin0or 6885 fiintim 6927 fisseneq 6930 djudom 7091 difinfsnlem 7097 nnnninfeq 7125 nnnninfeq2 7126 enomnilem 7135 enmkvlem 7158 enwomnilem 7166 exmidapne 7258 prmuloc 7564 cauappcvgprlemopl 7644 cauappcvgprlemdisj 7649 cauappcvgprlemladdfl 7653 caucvgprlemopl 7667 axcaucvglemcau 7896 xnn0letri 9802 xaddf 9843 xleaddadd 9886 ssfzo12bi 10224 rebtwn2zlemstep 10252 btwnzge0 10299 addmodlteq 10397 frecuzrdgg 10415 qsqeqor 10630 apexp1 10697 hashxp 10805 cjap 10914 caucvgre 10989 minmax 11237 xrminmax 11272 sumeq2 11366 fsumconst 11461 ntrivcvgap 11555 prodeq2 11564 p1modz1 11800 bezoutlemmain 11998 dfgcd2 12014 uzwodc 12037 lcmgcdlem 12076 mulgval 12985 cnpnei 13655 cnntr 13661 txmetcnp 13954 lgsval 14341 pw1nct 14688 peano4nninf 14691 |
Copyright terms: Public domain | W3C validator |