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  7345  prmuloc  7652  cauappcvgprlemopl  7732  cauappcvgprlemdisj  7737  cauappcvgprlemladdfl  7741  caucvgprlemopl  7755  axcaucvglemcau  7984  xnn0letri  9897  xaddf  9938  xleaddadd  9981  ssfzo12bi  10320  rebtwn2zlemstep  10361  btwnzge0  10409  addmodlteq  10509  frecuzrdgg  10527  qsqeqor  10761  apexp1  10829  hashxp  10937  cjap  11090  caucvgre  11165  minmax  11414  xrminmax  11449  sumeq2  11543  fsumconst  11638  ntrivcvgap  11732  prodeq2  11741  p1modz1  11978  bezoutlemmain  12192  dfgcd2  12208  uzwodc  12231  nninfctlemfo  12234  lcmgcdlem  12272  4sqexercise2  12595  4sqlemsdc  12596  mulgval  13330  cnpnei  14541  cnntr  14547  txmetcnp  14840  mpomulcn  14888  lgsval  15331  pw1nct  15736  peano4nninf  15739