Theorem ad3antlr 497

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 493	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 276	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antlr  499  nntr2  6780  phpm  7172  phplem4on  7174  fidifsnen  7177  fisbth  7192  fin0  7194  fin0or  7195  fiintim  7243  fisseneq  7247  djudom  7440  difinfsnlem  7446  nnnninfeq  7475  nnnninfeq2  7476  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  exmidapne  7633  prmuloc  7940  cauappcvgprlemopl  8020  cauappcvgprlemdisj  8025  cauappcvgprlemladdfl  8029  caucvgprlemopl  8043  axcaucvglemcau  8272  xnn0letri  10223  xaddf  10264  xleaddadd  10307  ssfzo12bi  10661  rebtwn2zlemstep  10705  btwnzge0  10757  addmodlteq  10857  frecuzrdgg  10875  qsqeqor  11109  apexp1  11179  hashxp  11290  ccatcl  11384  swrdccat3blem  11534  cjap  11695  caucvgre  11770  minmax  12021  xrminmax  12057  sumeq2  12151  fsumconst  12247  ntrivcvgap  12341  prodeq2  12350  p1modz1  12587  bezoutlemmain  12801  dfgcd2  12817  uzwodc  12840  nninfctlemfo  12843  lcmgcdlem  12881  pwbdvdseu  12973  sqrtrirr  13015  4sqexercise2  13208  4sqlemsdc  13209  mulgval  13985  gsumconstcmn  14267  psrass1fi  15206  cnpnei  15457  cnntr  15463  txmetcnp  15756  mpomulcn  15804  lgsval  16340  upgriswlkdc  16818  pw1nct  17250  peano4nninf  17267