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  6596  phpm  6969  phplem4on  6971  fidifsnen  6974  fisbth  6987  fin0  6989  fin0or  6990  fiintim  7035  fisseneq  7038  djudom  7202  difinfsnlem  7208  nnnninfeq  7237  nnnninfeq2  7238  enomnilem  7247  enmkvlem  7270  enwomnilem  7278  exmidapne  7379  prmuloc  7686  cauappcvgprlemopl  7766  cauappcvgprlemdisj  7771  cauappcvgprlemladdfl  7775  caucvgprlemopl  7789  axcaucvglemcau  8018  xnn0letri  9932  xaddf  9973  xleaddadd  10016  ssfzo12bi  10361  rebtwn2zlemstep  10402  btwnzge0  10450  addmodlteq  10550  frecuzrdgg  10568  qsqeqor  10802  apexp1  10870  hashxp  10978  ccatcl  11057  cjap  11261  caucvgre  11336  minmax  11585  xrminmax  11620  sumeq2  11714  fsumconst  11809  ntrivcvgap  11903  prodeq2  11912  p1modz1  12149  bezoutlemmain  12363  dfgcd2  12379  uzwodc  12402  nninfctlemfo  12405  lcmgcdlem  12443  4sqexercise2  12766  4sqlemsdc  12767  mulgval  13502  cnpnei  14735  cnntr  14741  txmetcnp  15034  mpomulcn  15082  lgsval  15525  pw1nct  16014  peano4nninf  16017