Theorem syl2an 349

Description: A double syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
syl2an	|- ((th /\ ta ) -> ch)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 |- ((ph /\ ps) -> ch)
2		syl2an.2	. . 3 |- (th -> ph)
3	1, 2	sylan 343	. 2 |- ((th /\ ps) -> ch)
4		syl2an.3	. 2 |- (ta -> ps)
5	3, 4	sylan2 346	1 |- ((th /\ ta ) -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  ssconb 1598  copsex2g 1903  breqan12d 2074  tz7.7 2224  ordin 2228  onin 2229  ontri1 2232  ordon 2238  onelpsst 2253  onsseleq 2254  ontr2 2259  peano4 2393  findsg 2398  vtoclr 2449  opthprc 2457  ssxp 2487  sotri 2630  funsn 2690  funco 2696  funssres 2698  fco 2760  cleqfv 2880  isofrlem 2939  tfrlem5 2953  tfrlem11 2959  tz7.48lem 2993  opreqan12d 3015  oacan 3150  oawordri 3152  oaass 3163  nnasuc 3168  nnmsuc 3169  nnacom 3175  nnaordi 3176  nnaword1 3186  nnmcan 3190  omsmo 3196  brecop 3242  ecopoprtrn 3247  th3qlem1 3250  ecoprdi 3257  mapvalg 3263  mapsn 3269  en2sn 3336  sbthlem7 3355  sbth 3359  sdomnsym 3364  xpen 3383  mapenlem1 3384  mapenlem2 3385  mapdom1 3387  mapdom2 3389  limenpsi 3400  phplem5 3407  php 3409  php3 3411  nndomo 3416  ominf 3423  pssnn 3428  unblem2 3432  isfinite2 3437  unfilem1 3438  unfilem2 3439  unfi2 3442  inf3lem6 3469  aceq5lem4 3561  kmlem6 3585  zornlem6 3608  fodom 3613  cardnn 3631  carddomi 3641  unxpdomlem 3649  unxpdom2 3651  ondomcard 3663  cdavalt 3716  cdafi 3730  axrepndlem2 3739  axrepnd 3740  ltsopi 3810  mulclpi 3815  addcompi 3816  mulcompi 3818  distrpi 3820  ltexpi 3823  ltapi 3824  ltmpi 3825  addcmpblnq 3846  mulpipq 3849  addclpq 3852  addasspq 3857  distrpq 3861  ltsopq 3869  ltexpq 3874  ltrpq 3879  genpnnp 3902  mulclprlem 3915  distrlem1pr 3921  distrlem5pr 3925  addcanpr 3946  reclem3pr 3952  mulcmpblnr 3977  addsrpr 3978  mulclsr 3987  mulasssr 3993  distrsr 3994  ltsosr 3997  1idsr 4001  00sr 4002  recexsrlem 4006  mulgt0sr 4008  suppsr3 4018  addcnsr 4047  axmulcl 4068  axmulass 4073  axdistr 4074  ax0id 4076  axcnre 4087  resubclt 4173  divmuldivt 4263  divdivdivt 4265  divdiv23t 4271  ltadd2t 4349  leadd2t 4351  ltsubadd2t 4354  lesubadd2t 4356  ltaddsub2t 4358  ltmuldiv2t 4407  ltdivmult 4408  lerec 4411  nnaddclt 4436  nnmulclt 4437  nn2get 4438  nnleltp1t 4448  nnltp1let 4449  nnaddm1clt 4452  nndiv 4453  nnreclt 4522  nn0leltp1t 4557  nn0ltlem1 4558  nn0subt 4587  zaddclt 4590  zsubclt 4591  znnsubt 4595  zmulclt 4596  zltp1let 4597  zleltp1t 4598  zneo 4601  peano2uz 4602  uzind 4603  uzwo 4605  nnwoOLD 4608  indstr 4611  zmax 4618  rebtwnz 4620  flgzt 4626  qret 4631  qnegclt 4643  qsubclt 4645  qrecclt 4646  qbtwnre 4650  om2uzlt 4654  om2uzf1o 4656  expp1t 4678  expaddt 4698  le2sqet 4707  nn0opthlem2 4723  sqrlem6 4736  sqrlem12 4742  sqrle 4765  sqr4 4772  sqr9 4773  sqr2irr 4782  nn0ennn 4925  xpnnen 4927  znnenlem 4929  znnen 4930  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  infxpabs 4949  infmap1 4950  hvsub4t 5014  his7 5051  normpyct 5093  ocorth 5172  chocuni 5179  projlem28 5220  projlem31 5223  pjpj0 5259  shscl 5282  chsupss 5311  shjvalt 5322  chjvalt 5323  shjclt 5329  chjclt 5330  shsvs 5337  shslej 5339  chslejt 5415  chjcomt 5423  chub1t 5424  chdmj1t 5442  spanunsn 5482  osumlem2 5531  spansncv 5542  5oalem1 5544  5oalem2 5545  5oalem3 5546  5oalem5 5548  3oalem2 5553  pjv 5589  cvcon3t 5716  dmdbr 5731  ssdmd1 5736  chrelat 5757  atcv0eq 5767  atcvatlem 5770  atcvat 5771  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780  mdsymlem8 5783

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org