Theorem ad4ant14 1293

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis

Ref	Expression
ad4ant14.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad4ant14	|- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant14.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 450	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	2a1d 26	. 2 |- ( ph -> ( th -> ( ta -> ( ps -> ch ) ) ) )
4	3	imp41 619	1 |- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  grprinvlem  6872  pntlem3  25298  hlpasch  25648  lfgrwlkprop  26584  wlkiswwlks1  26753  frgrnbnb  27157  frgr2wwlkeqm  27195  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem26  33435  mblfinlem2  33447  ssfiunibd  39523  xralrple2  39570  infleinf  39588  infxrpnf  39674  fprodcn  39832  limsupub  39936  limsuppnflem  39942  limsupmnflem  39952  cnrefiisplem  40055  climxlim2lem  40071  icccncfext  40100  cncficcgt0  40101  cncfioobd  40110  dvbdfbdioolem2  40144  itgspltprt  40195  stoweidlem34  40251  stoweidlem49  40266  stoweidlem57  40274  fourierdlem34  40358  fourierdlem39  40363  fourierdlem50  40373  fourierdlem51  40374  fourierdlem64  40387  fourierdlem73  40396  fourierdlem77  40400  fourierdlem81  40404  fourierdlem94  40417  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fourier2  40444  etransclem24  40475  intsal  40548  sge0pr  40611  sge0iunmptlemfi  40630  sge0seq  40663  sge0reuz  40664  nnfoctbdjlem  40672  meadjiunlem  40682  ismeannd  40684  carageniuncllem2  40736  isomennd  40745  hoicvr  40762  hspmbllem2  40841  iunhoiioolem  40889  iunhoiioo  40890  vonioo  40896  vonicc  40899  preimageiingt  40930  preimaleiinlt  40931  smfaddlem1  40971  smfaddlem2  40972  smflimlem4  40982  smfrec  40996  smfinflem  41023  lighneallem3  41524  sprsymrelf1lem  41741