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  6671  phpm  7052  phplem4on  7054  fidifsnen  7057  fisbth  7072  fin0  7074  fin0or  7075  fiintim  7123  fisseneq  7127  djudom  7292  difinfsnlem  7298  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  exmidapne  7479  prmuloc  7786  cauappcvgprlemopl  7866  cauappcvgprlemdisj  7871  cauappcvgprlemladdfl  7875  caucvgprlemopl  7889  axcaucvglemcau  8118  xnn0letri  10038  xaddf  10079  xleaddadd  10122  ssfzo12bi  10471  rebtwn2zlemstep  10513  btwnzge0  10561  addmodlteq  10661  frecuzrdgg  10679  qsqeqor  10913  apexp1  10981  hashxp  11091  ccatcl  11171  swrdccat3blem  11321  cjap  11468  caucvgre  11543  minmax  11792  xrminmax  11827  sumeq2  11921  fsumconst  12017  ntrivcvgap  12111  prodeq2  12120  p1modz1  12357  bezoutlemmain  12571  dfgcd2  12587  uzwodc  12610  nninfctlemfo  12613  lcmgcdlem  12651  4sqexercise2  12974  4sqlemsdc  12975  mulgval  13711  cnpnei  14946  cnntr  14952  txmetcnp  15245  mpomulcn  15293  lgsval  15736  upgriswlkdc  16214  pw1nct  16625  peano4nninf  16629