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  6561  phpm  6926  phplem4on  6928  fidifsnen  6931  fisbth  6944  fin0  6946  fin0or  6947  fiintim  6992  fisseneq  6995  djudom  7159  difinfsnlem  7165  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  exmidapne  7327  prmuloc  7633  cauappcvgprlemopl  7713  cauappcvgprlemdisj  7718  cauappcvgprlemladdfl  7722  caucvgprlemopl  7736  axcaucvglemcau  7965  xnn0letri  9878  xaddf  9919  xleaddadd  9962  ssfzo12bi  10301  rebtwn2zlemstep  10342  btwnzge0  10390  addmodlteq  10490  frecuzrdgg  10508  qsqeqor  10742  apexp1  10810  hashxp  10918  cjap  11071  caucvgre  11146  minmax  11395  xrminmax  11430  sumeq2  11524  fsumconst  11619  ntrivcvgap  11713  prodeq2  11722  p1modz1  11959  bezoutlemmain  12165  dfgcd2  12181  uzwodc  12204  nninfctlemfo  12207  lcmgcdlem  12245  4sqexercise2  12568  4sqlemsdc  12569  mulgval  13252  cnpnei  14455  cnntr  14461  txmetcnp  14754  mpomulcn  14802  lgsval  15245  pw1nct  15647  peano4nninf  15650