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  6619  phpm  6995  phplem4on  6997  fidifsnen  7000  fisbth  7013  fin0  7015  fin0or  7016  fiintim  7061  fisseneq  7064  djudom  7228  difinfsnlem  7234  nnnninfeq  7263  nnnninfeq2  7264  enomnilem  7273  enmkvlem  7296  enwomnilem  7304  exmidapne  7414  prmuloc  7721  cauappcvgprlemopl  7801  cauappcvgprlemdisj  7806  cauappcvgprlemladdfl  7810  caucvgprlemopl  7824  axcaucvglemcau  8053  xnn0letri  9967  xaddf  10008  xleaddadd  10051  ssfzo12bi  10398  rebtwn2zlemstep  10439  btwnzge0  10487  addmodlteq  10587  frecuzrdgg  10605  qsqeqor  10839  apexp1  10907  hashxp  11015  ccatcl  11094  swrdccat3blem  11237  cjap  11383  caucvgre  11458  minmax  11707  xrminmax  11742  sumeq2  11836  fsumconst  11931  ntrivcvgap  12025  prodeq2  12034  p1modz1  12271  bezoutlemmain  12485  dfgcd2  12501  uzwodc  12524  nninfctlemfo  12527  lcmgcdlem  12565  4sqexercise2  12888  4sqlemsdc  12889  mulgval  13625  cnpnei  14858  cnntr  14864  txmetcnp  15157  mpomulcn  15205  lgsval  15648  pw1nct  16280  peano4nninf  16283