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  6657  phpm  7035  phplem4on  7037  fidifsnen  7040  fisbth  7053  fin0  7055  fin0or  7056  fiintim  7101  fisseneq  7104  djudom  7268  difinfsnlem  7274  nnnninfeq  7303  nnnninfeq2  7304  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  exmidapne  7454  prmuloc  7761  cauappcvgprlemopl  7841  cauappcvgprlemdisj  7846  cauappcvgprlemladdfl  7850  caucvgprlemopl  7864  axcaucvglemcau  8093  xnn0letri  10007  xaddf  10048  xleaddadd  10091  ssfzo12bi  10439  rebtwn2zlemstep  10480  btwnzge0  10528  addmodlteq  10628  frecuzrdgg  10646  qsqeqor  10880  apexp1  10948  hashxp  11056  ccatcl  11136  swrdccat3blem  11279  cjap  11425  caucvgre  11500  minmax  11749  xrminmax  11784  sumeq2  11878  fsumconst  11973  ntrivcvgap  12067  prodeq2  12076  p1modz1  12313  bezoutlemmain  12527  dfgcd2  12543  uzwodc  12566  nninfctlemfo  12569  lcmgcdlem  12607  4sqexercise2  12930  4sqlemsdc  12931  mulgval  13667  cnpnei  14901  cnntr  14907  txmetcnp  15200  mpomulcn  15248  lgsval  15691  upgriswlkdc  16081  pw1nct  16398  peano4nninf  16402