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  6738  phpm  7122  phplem4on  7124  fidifsnen  7127  fisbth  7142  fin0  7144  fin0or  7145  fiintim  7193  fisseneq  7197  djudom  7386  difinfsnlem  7392  nnnninfeq  7421  nnnninfeq2  7422  enomnilem  7431  enmkvlem  7454  enwomnilem  7462  exmidapne  7579  prmuloc  7886  cauappcvgprlemopl  7966  cauappcvgprlemdisj  7971  cauappcvgprlemladdfl  7975  caucvgprlemopl  7989  axcaucvglemcau  8218  xnn0letri  10142  xaddf  10183  xleaddadd  10226  ssfzo12bi  10577  rebtwn2zlemstep  10619  btwnzge0  10667  addmodlteq  10767  frecuzrdgg  10785  qsqeqor  11019  apexp1  11088  hashxp  11199  ccatcl  11289  swrdccat3blem  11439  cjap  11599  caucvgre  11674  minmax  11923  xrminmax  11958  sumeq2  12052  fsumconst  12148  ntrivcvgap  12242  prodeq2  12251  p1modz1  12488  bezoutlemmain  12702  dfgcd2  12718  uzwodc  12741  nninfctlemfo  12744  lcmgcdlem  12782  4sqexercise2  13105  4sqlemsdc  13106  mulgval  13860  cnpnei  15133  cnntr  15139  txmetcnp  15432  mpomulcn  15480  lgsval  15926  upgriswlkdc  16404  pw1nct  16826  peano4nninf  16833