Theorem ad3antlr 493

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antlr	⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad2antlr 489	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 276	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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