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  6556  phpm  6921  phplem4on  6923  fidifsnen  6926  fisbth  6939  fin0  6941  fin0or  6942  fiintim  6985  fisseneq  6988  djudom  7152  difinfsnlem  7158  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  exmidapne  7320  prmuloc  7626  cauappcvgprlemopl  7706  cauappcvgprlemdisj  7711  cauappcvgprlemladdfl  7715  caucvgprlemopl  7729  axcaucvglemcau  7958  xnn0letri  9869  xaddf  9910  xleaddadd  9953  ssfzo12bi  10292  rebtwn2zlemstep  10321  btwnzge0  10369  addmodlteq  10469  frecuzrdgg  10487  qsqeqor  10721  apexp1  10789  hashxp  10897  cjap  11050  caucvgre  11125  minmax  11373  xrminmax  11408  sumeq2  11502  fsumconst  11597  ntrivcvgap  11691  prodeq2  11700  p1modz1  11937  bezoutlemmain  12135  dfgcd2  12151  uzwodc  12174  nninfctlemfo  12177  lcmgcdlem  12215  4sqexercise2  12537  4sqlemsdc  12538  mulgval  13192  cnpnei  14387  cnntr  14393  txmetcnp  14686  lgsval  15120  pw1nct  15493  peano4nninf  15496