Theorem syl6an 568

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

Hypotheses

Ref	Expression
syl6an.1	|- ( ph -> ps )
syl6an.2	|- ( ph -> ( ch -> th ) )
syl6an.3	|- ( ( ps /\ th ) -> ta )

Assertion

Ref	Expression
syl6an	|- ( ph -> ( ch -> ta ) )

Proof of Theorem syl6an

Step	Hyp	Ref	Expression
1		syl6an.2	. . 3 |- ( ph -> ( ch -> th ) )
2		syl6an.1	. . 3 |- ( ph -> ps )
3	1, 2	jctild 566	. 2 |- ( ph -> ( ch -> ( ps /\ th ) ) )
4		syl6an.3	. 2 |- ( ( ps /\ th ) -> ta )
5	3, 4	syl6 35	1 |- ( ph -> ( ch -> ta ) )

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:  dfsb2  2373  xpcan  5570  xpcan2  5571  mapxpen  8126  sucdom2  8156  f1finf1o  8187  unfi  8227  inf3lem3  8527  dfac12r  8968  cfsuc  9079  fin23lem26  9147  iundom2g  9362  inar1  9597  rankcf  9599  ltsrpr  9898  supsrlem  9932  axpre-sup  9990  nominpos  11269  ublbneg  11773  qbtwnre  12030  fsequb  12774  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  rexanre  14086  rexuzre  14092  rexico  14093  caubnd  14098  rlim2lt  14228  rlim3  14229  lo1bddrp  14256  o1lo1  14268  climshftlem  14305  rlimcn2  14321  rlimo1  14347  lo1add  14357  lo1mul  14358  lo1le  14382  isercoll  14398  serf0  14411  cvgcmp  14548  dvds1lem  14993  dvds2lem  14994  isprm5  15419  vdwlem2  15686  vdwlem10  15694  vdwlem11  15695  lsmcv  19141  lmconst  21065  ptcnplem  21424  fclscmp  21834  tsmsres  21947  addcnlem  22667  lebnumlem3  22762  xlebnum  22764  lebnumii  22765  iscmet3lem2  23090  bcthlem4  23124  cniccbdd  23230  ovoliunlem2  23271  mbfi1flimlem  23489  ply1divex  23896  aalioulem3  24089  aalioulem5  24091  aalioulem6  24092  aaliou  24093  ulmshftlem  24143  ulmbdd  24152  tanarg  24365  cxploglim  24704  ftalem2  24800  ftalem7  24805  dchrisumlem3  25180  frgrogt3nreg  27255  ubthlem3  27728  spansncol  28427  riesz1  28924  erdsze2lem2  31186  dfrdg4  32058  neibastop2  32356  onsuct0  32440  bj-bary1  33162  topdifinffinlem  33195  poimirlem24  33433  incsequz  33544  caushft  33557  equivbnd  33589  cntotbnd  33595  4atexlemex4  35359  frege124d  38053  gneispace  38432  expgrowth  38534  vk15.4j  38734  sstrALT2  39070  iccpartdisj  41373  ccats1pfxeqrex  41422