Theorem ad3antlr 485

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 481	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 274	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4antlr  487  nntr2  6462  phpm  6822  phplem4on  6824  fidifsnen  6827  fisbth  6840  fin0  6842  fin0or  6843  fiintim  6885  fisseneq  6888  djudom  7049  difinfsnlem  7055  nnnninfeq  7083  nnnninfeq2  7084  enomnilem  7093  enmkvlem  7116  enwomnilem  7124  prmuloc  7498  cauappcvgprlemopl  7578  cauappcvgprlemdisj  7583  cauappcvgprlemladdfl  7587  caucvgprlemopl  7601  axcaucvglemcau  7830  xnn0letri  9730  xaddf  9771  xleaddadd  9814  ssfzo12bi  10150  rebtwn2zlemstep  10178  btwnzge0  10225  addmodlteq  10323  frecuzrdgg  10341  apexp1  10620  hashxp  10728  cjap  10834  caucvgre  10909  minmax  11157  xrminmax  11192  sumeq2  11286  fsumconst  11381  ntrivcvgap  11475  prodeq2  11484  p1modz1  11720  bezoutlemmain  11916  dfgcd2  11932  lcmgcdlem  11988  cnpnei  12760  cnntr  12766  txmetcnp  13059  pw1nct  13717  peano4nninf  13720