Theorem syl5com 52

Description: Syllogism inference with commuted antecedents.

Hypotheses

Ref	Expression
syl5com.2	|- (ph -> (ps -> ch))
syl5com.1	|- (th -> ps)

Assertion

Ref	Expression
syl5com	|- (th -> (ph -> ch))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- (th -> ps)
2	1	a1d 12	. 2 |- (th -> (ph -> ps))
3		syl5com.2	. 2 |- (ph -> (ps -> ch))
4	2, 3	sylcom 51	1 |- (th -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  ax16i 1270  mo 1393  2mo 1447  ceqsalg 1825  cgsexg 1831  cgsex2g 1832  cgsex4g 1833  cla42egv 1864  cla43egv 1866  disjne 2315  ordelord 2970  trsuc 3055  ordsuc 3065  sucssel 3070  tfi 3126  peano5 3153  asymref2 3440  funssres 3552  f1dmex 3710  fvimacnv 3805  isorel 3894  tz7.49 3959  oeworde 4220  erth 4282  dom2d 4403  enen2 4476  domen2 4478  2pwuninel 4485  carden 4823  sdomsdomcard 4840  alephordi 4866  alephsucdom 4872  addcanpr 5144  xrub 6068  uzwo3lem2 6205  fseqsupcl 6511  fseqsupub 6512  facndivt 6928  bccl2t 6956  clmi1 7071  infxpidmlem10 7546  inopnt 7585  basis1t 7599  tgclt 7609  tgsst 7621  elcls3 7696  opnuni 7853  neibl 7862  metcnp 7872  grpass 8032  ablcom 8088  shaddclt 9070  shaddcltOLD 9071  shmulclt 9072  shmulcltOLD 9073  hlimunii 9093  projlem15 9185  projlem22 9192  projlem26 9196  shlej1t 9340  spansnss2t 9483  adjt 9842  nlelch 9979  pjorthco 10082  stge0t 10136  stle1t 10137  stjt 10147  mdsl1 10233  irredlem1 10302  mdsymlem5 10319  fiiu 10433  fiiu2 10462  homcard 10511  filintf 10528  imonclem 10682

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

Copyright terms: Public domain