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  6735  phpm  7119  phplem4on  7121  fidifsnen  7124  fisbth  7139  fin0  7141  fin0or  7142  fiintim  7190  fisseneq  7194  djudom  7383  difinfsnlem  7389  nnnninfeq  7418  nnnninfeq2  7419  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  exmidapne  7570  prmuloc  7877  cauappcvgprlemopl  7957  cauappcvgprlemdisj  7962  cauappcvgprlemladdfl  7966  caucvgprlemopl  7980  axcaucvglemcau  8209  xnn0letri  10132  xaddf  10173  xleaddadd  10216  ssfzo12bi  10566  rebtwn2zlemstep  10608  btwnzge0  10656  addmodlteq  10756  frecuzrdgg  10774  qsqeqor  11008  apexp1  11076  hashxp  11186  ccatcl  11274  swrdccat3blem  11424  cjap  11584  caucvgre  11659  minmax  11908  xrminmax  11943  sumeq2  12037  fsumconst  12133  ntrivcvgap  12227  prodeq2  12236  p1modz1  12473  bezoutlemmain  12687  dfgcd2  12703  uzwodc  12726  nninfctlemfo  12729  lcmgcdlem  12767  4sqexercise2  13090  4sqlemsdc  13091  mulgval  13828  cnpnei  15071  cnntr  15077  txmetcnp  15370  mpomulcn  15418  lgsval  15864  upgriswlkdc  16342  pw1nct  16764  peano4nninf  16771