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  6662  phpm  7040  phplem4on  7042  fidifsnen  7045  fisbth  7058  fin0  7060  fin0or  7061  fiintim  7109  fisseneq  7112  djudom  7276  difinfsnlem  7282  nnnninfeq  7311  nnnninfeq2  7312  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  exmidapne  7462  prmuloc  7769  cauappcvgprlemopl  7849  cauappcvgprlemdisj  7854  cauappcvgprlemladdfl  7858  caucvgprlemopl  7872  axcaucvglemcau  8101  xnn0letri  10016  xaddf  10057  xleaddadd  10100  ssfzo12bi  10448  rebtwn2zlemstep  10489  btwnzge0  10537  addmodlteq  10637  frecuzrdgg  10655  qsqeqor  10889  apexp1  10957  hashxp  11066  ccatcl  11146  swrdccat3blem  11292  cjap  11438  caucvgre  11513  minmax  11762  xrminmax  11797  sumeq2  11891  fsumconst  11986  ntrivcvgap  12080  prodeq2  12089  p1modz1  12326  bezoutlemmain  12540  dfgcd2  12556  uzwodc  12579  nninfctlemfo  12582  lcmgcdlem  12620  4sqexercise2  12943  4sqlemsdc  12944  mulgval  13680  cnpnei  14914  cnntr  14920  txmetcnp  15213  mpomulcn  15261  lgsval  15704  upgriswlkdc  16132  pw1nct  16482  peano4nninf  16486