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  6776  phpm  7167  phplem4on  7169  fidifsnen  7172  fisbth  7187  fin0  7189  fin0or  7190  fiintim  7238  fisseneq  7242  djudom  7433  difinfsnlem  7439  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  exmidapne  7626  prmuloc  7933  cauappcvgprlemopl  8013  cauappcvgprlemdisj  8018  cauappcvgprlemladdfl  8022  caucvgprlemopl  8036  axcaucvglemcau  8265  xnn0letri  10207  xaddf  10248  xleaddadd  10291  ssfzo12bi  10645  rebtwn2zlemstep  10689  btwnzge0  10737  addmodlteq  10837  frecuzrdgg  10855  qsqeqor  11089  apexp1  11158  hashxp  11269  ccatcl  11363  swrdccat3blem  11513  cjap  11674  caucvgre  11749  minmax  11998  xrminmax  12033  sumeq2  12127  fsumconst  12223  ntrivcvgap  12317  prodeq2  12326  p1modz1  12563  bezoutlemmain  12777  dfgcd2  12793  uzwodc  12816  nninfctlemfo  12819  lcmgcdlem  12857  4sqexercise2  13180  4sqlemsdc  13181  mulgval  13927  gsumconstcmn  14168  cnpnei  15322  cnntr  15328  txmetcnp  15621  mpomulcn  15669  lgsval  16135  upgriswlkdc  16613  pw1nct  17045  peano4nninf  17061