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  6664  phpm  7045  phplem4on  7047  fidifsnen  7050  fisbth  7063  fin0  7065  fin0or  7066  fiintim  7114  fisseneq  7117  djudom  7281  difinfsnlem  7287  nnnninfeq  7316  nnnninfeq2  7317  enomnilem  7326  enmkvlem  7349  enwomnilem  7357  exmidapne  7467  prmuloc  7774  cauappcvgprlemopl  7854  cauappcvgprlemdisj  7859  cauappcvgprlemladdfl  7863  caucvgprlemopl  7877  axcaucvglemcau  8106  xnn0letri  10026  xaddf  10067  xleaddadd  10110  ssfzo12bi  10458  rebtwn2zlemstep  10500  btwnzge0  10548  addmodlteq  10648  frecuzrdgg  10666  qsqeqor  10900  apexp1  10968  hashxp  11077  ccatcl  11157  swrdccat3blem  11307  cjap  11454  caucvgre  11529  minmax  11778  xrminmax  11813  sumeq2  11907  fsumconst  12002  ntrivcvgap  12096  prodeq2  12105  p1modz1  12342  bezoutlemmain  12556  dfgcd2  12572  uzwodc  12595  nninfctlemfo  12598  lcmgcdlem  12636  4sqexercise2  12959  4sqlemsdc  12960  mulgval  13696  cnpnei  14930  cnntr  14936  txmetcnp  15229  mpomulcn  15277  lgsval  15720  upgriswlkdc  16148  pw1nct  16514  peano4nninf  16518