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  6570  phpm  6935  phplem4on  6937  fidifsnen  6940  fisbth  6953  fin0  6955  fin0or  6956  fiintim  7001  fisseneq  7004  djudom  7168  difinfsnlem  7174  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  exmidapne  7343  prmuloc  7650  cauappcvgprlemopl  7730  cauappcvgprlemdisj  7735  cauappcvgprlemladdfl  7739  caucvgprlemopl  7753  axcaucvglemcau  7982  xnn0letri  9895  xaddf  9936  xleaddadd  9979  ssfzo12bi  10318  rebtwn2zlemstep  10359  btwnzge0  10407  addmodlteq  10507  frecuzrdgg  10525  qsqeqor  10759  apexp1  10827  hashxp  10935  cjap  11088  caucvgre  11163  minmax  11412  xrminmax  11447  sumeq2  11541  fsumconst  11636  ntrivcvgap  11730  prodeq2  11739  p1modz1  11976  bezoutlemmain  12190  dfgcd2  12206  uzwodc  12229  nninfctlemfo  12232  lcmgcdlem  12270  4sqexercise2  12593  4sqlemsdc  12594  mulgval  13328  cnpnei  14539  cnntr  14545  txmetcnp  14838  mpomulcn  14886  lgsval  15329  pw1nct  15734  peano4nninf  15737