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  6666  phpm  7047  phplem4on  7049  fidifsnen  7052  fisbth  7067  fin0  7069  fin0or  7070  fiintim  7118  fisseneq  7121  djudom  7286  difinfsnlem  7292  nnnninfeq  7321  nnnninfeq2  7322  enomnilem  7331  enmkvlem  7354  enwomnilem  7362  exmidapne  7472  prmuloc  7779  cauappcvgprlemopl  7859  cauappcvgprlemdisj  7864  cauappcvgprlemladdfl  7868  caucvgprlemopl  7882  axcaucvglemcau  8111  xnn0letri  10031  xaddf  10072  xleaddadd  10115  ssfzo12bi  10463  rebtwn2zlemstep  10505  btwnzge0  10553  addmodlteq  10653  frecuzrdgg  10671  qsqeqor  10905  apexp1  10973  hashxp  11083  ccatcl  11163  swrdccat3blem  11313  cjap  11460  caucvgre  11535  minmax  11784  xrminmax  11819  sumeq2  11913  fsumconst  12008  ntrivcvgap  12102  prodeq2  12111  p1modz1  12348  bezoutlemmain  12562  dfgcd2  12578  uzwodc  12601  nninfctlemfo  12604  lcmgcdlem  12642  4sqexercise2  12965  4sqlemsdc  12966  mulgval  13702  cnpnei  14936  cnntr  14942  txmetcnp  15235  mpomulcn  15283  lgsval  15726  upgriswlkdc  16171  pw1nct  16554  peano4nninf  16558