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  6676  phpm  7057  phplem4on  7059  fidifsnen  7062  fisbth  7077  fin0  7079  fin0or  7080  fiintim  7128  fisseneq  7132  djudom  7297  difinfsnlem  7303  nnnninfeq  7332  nnnninfeq2  7333  enomnilem  7342  enmkvlem  7365  enwomnilem  7373  exmidapne  7484  prmuloc  7791  cauappcvgprlemopl  7871  cauappcvgprlemdisj  7876  cauappcvgprlemladdfl  7880  caucvgprlemopl  7894  axcaucvglemcau  8123  xnn0letri  10043  xaddf  10084  xleaddadd  10127  ssfzo12bi  10476  rebtwn2zlemstep  10518  btwnzge0  10566  addmodlteq  10666  frecuzrdgg  10684  qsqeqor  10918  apexp1  10986  hashxp  11096  ccatcl  11179  swrdccat3blem  11329  cjap  11489  caucvgre  11564  minmax  11813  xrminmax  11848  sumeq2  11942  fsumconst  12038  ntrivcvgap  12132  prodeq2  12141  p1modz1  12378  bezoutlemmain  12592  dfgcd2  12608  uzwodc  12631  nninfctlemfo  12634  lcmgcdlem  12672  4sqexercise2  12995  4sqlemsdc  12996  mulgval  13732  cnpnei  14972  cnntr  14978  txmetcnp  15271  mpomulcn  15319  lgsval  15762  upgriswlkdc  16240  pw1nct  16664  peano4nninf  16671