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  6749  phpm  7133  phplem4on  7135  fidifsnen  7138  fisbth  7153  fin0  7155  fin0or  7156  fiintim  7204  fisseneq  7208  djudom  7397  difinfsnlem  7403  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  exmidapne  7590  prmuloc  7897  cauappcvgprlemopl  7977  cauappcvgprlemdisj  7982  cauappcvgprlemladdfl  7986  caucvgprlemopl  8000  axcaucvglemcau  8229  xnn0letri  10158  xaddf  10199  xleaddadd  10242  ssfzo12bi  10595  rebtwn2zlemstep  10639  btwnzge0  10687  addmodlteq  10787  frecuzrdgg  10805  qsqeqor  11039  apexp1  11108  hashxp  11219  ccatcl  11309  swrdccat3blem  11459  cjap  11619  caucvgre  11694  minmax  11943  xrminmax  11978  sumeq2  12072  fsumconst  12168  ntrivcvgap  12262  prodeq2  12271  p1modz1  12508  bezoutlemmain  12722  dfgcd2  12738  uzwodc  12761  nninfctlemfo  12764  lcmgcdlem  12802  4sqexercise2  13125  4sqlemsdc  13126  mulgval  13878  cnpnei  15213  cnntr  15219  txmetcnp  15512  mpomulcn  15560  lgsval  16006  upgriswlkdc  16484  pw1nct  16916  peano4nninf  16923