Theorem ad4ant14 752

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant14	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 715	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 715	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ad5ant15  758  ad5ant25  761  soisoi  7285  dfac9  10066  lediv12a  12052  leexp1a  14116  seqcoll  14405  lo1bdd2  15466  rlimcld2  15520  rlimcn1  15530  isercolllem1  15607  summo  15659  climcnds  15793  geomulcvg  15818  mertenslem2  15827  prodmolem2  15877  prodmo  15878  fprod2d  15923  pwsle  17431  isacs2  17590  grpinvalem  18576  gsumpropd2lem  18582  gsumwsubmcl  18740  gsumwmhm  18748  mulgfval  18977  gaid  19207  gsmsymgrfixlem1  19333  mulgnn0di  19731  gsumval3  19813  subrngint  20445  fvmptnn04if  22712  cnpnei  23127  lfinun  23388  xkopt  23518  isr0  23600  fbflim  23839  alexsubALTlem3  23912  metss  24372  iscmet3lem2  25168  ovoliunlem3  25381  mbfposr  25529  i1fmulclem  25579  itg10a  25587  iblss  25682  dvlip  25874  plyeq0lem  26091  mtest  26289  itgulm  26293  dchrisumlem3  27378  rpvmasum2  27399  pntlem3  27496  nosupbday  27593  noinfbday  27608  hlpasch  28659  f1otrg  28774  lfgrwlkprop  29589  wlkiswwlks1  29770  frgrnbnb  30195  frgr2wwlkeqm  30233  unidifsnne  32438  hashxpe  32705  ccatf1  32843  fxpsubm  33102  cos9thpiminplylem1  33745  signstfvneq0  34536  bnj605  34870  matunitlindflem1  37583  matunitlindflem2  37584  poimirlem26  37613  mblfinlem2  37625  ssfiunibd  45280  xralrple2  45323  infleinf  45341  infxrpnf  45415  fprodcn  45571  limsupub  45675  limsuppnflem  45681  limsupmnflem  45691  cnrefiisplem  45800  climxlim2lem  45816  icccncfext  45858  cncficcgt0  45859  cncfioobd  45868  dvbdfbdioolem2  45900  dvmptfprod  45916  itgspltprt  45950  stoweidlem34  46005  stoweidlem49  46020  stoweidlem57  46028  fourierdlem34  46112  fourierdlem39  46117  fourierdlem50  46127  fourierdlem51  46128  fourierdlem64  46141  fourierdlem73  46150  fourierdlem77  46154  fourierdlem81  46158  fourierdlem94  46171  fourierdlem97  46174  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  fourier2  46198  etransclem24  46229  intsal  46301  sge0pr  46365  sge0iunmptlemfi  46384  sge0seq  46417  sge0reuz  46418  nnfoctbdjlem  46426  meadjiunlem  46436  ismeannd  46438  carageniuncllem2  46493  isomennd  46502  hoicvr  46519  hspmbllem2  46598  iunhoiioolem  46646  iunhoiioo  46647  vonioo  46653  vonicc  46656  preimageiingt  46691  preimaleiinlt  46692  smfaddlem1  46734  smfaddlem2  46735  smflimlem4  46745  smfrec  46760  smfinflem  46788  sprsymrelf1lem  47465  lighneallem3  47581  1arymaptfo  48605