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 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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  499  nntr2  6770  phpm  7161  phplem4on  7163  fidifsnen  7166  fisbth  7181  fin0  7183  fin0or  7184  fiintim  7232  fisseneq  7236  djudom  7427  difinfsnlem  7433  nnnninfeq  7462  nnnninfeq2  7463  enomnilem  7472  enmkvlem  7495  enwomnilem  7503  exmidapne  7620  prmuloc  7927  cauappcvgprlemopl  8007  cauappcvgprlemdisj  8012  cauappcvgprlemladdfl  8016  caucvgprlemopl  8030  axcaucvglemcau  8259  xnn0letri  10188  xaddf  10229  xleaddadd  10272  ssfzo12bi  10626  rebtwn2zlemstep  10670  btwnzge0  10718  addmodlteq  10818  frecuzrdgg  10836  qsqeqor  11070  apexp1  11139  hashxp  11250  ccatcl  11344  swrdccat3blem  11494  cjap  11655  caucvgre  11730  minmax  11979  xrminmax  12014  sumeq2  12108  fsumconst  12204  ntrivcvgap  12298  prodeq2  12307  p1modz1  12544  bezoutlemmain  12758  dfgcd2  12774  uzwodc  12797  nninfctlemfo  12800  lcmgcdlem  12838  4sqexercise2  13161  4sqlemsdc  13162  mulgval  13908  gsumconstcmn  14149  cnpnei  15303  cnntr  15309  txmetcnp  15602  mpomulcn  15650  lgsval  16106  upgriswlkdc  16584  pw1nct  17016  peano4nninf  17023