HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 syl5com.1 . . 3 |- (th -> ps)
21a1d 12 . 2 |- (th -> (ph -> ps))
3 syl5com.2 . 2 |- (ph -> (ps -> ch))
42, 3sylcom 51 1 |- (th -> (ph -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  ax16i 1265  mo 1386  2mo 1440  ceqsalg 1816  cgsexg 1822  cgsex2g 1823  cgsex4g 1824  cla42egv 1855  cla43egv 1857  disjne 2305  ordelord 2960  trsuc 3045  ordsuc 3055  sucssel 3060  tfi 3116  peano5 3143  asymref2 3424  asymref2OLD 3426  funssres 3538  f1dmex 3695  fvimacnv 3790  isorel 3879  tz7.49 3944  oeworde 4204  erth 4266  dom2d 4385  enen2 4458  domen2 4460  carden 4803  sdomsdomcard 4820  alephordi 4846  alephsucdom 4852  addcanpr 5124  xrub 6027  uzwo3lem2 6165  fseqsupcl 6457  fseqsupub 6458  facndivt 6880  bccl2t 6909  clmi1 7024  infxpidmlem10 7504  inopnt 7542  basis1t 7556  tgclt 7566  tgsst 7578  elcls3 7652  opnuni 7808  neibl 7817  metcnp 7826  grpass 7981  ablcom 8039  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  hlimunii 9029  projlem15 9116  projlem22 9123  projlem26 9127  shlej1t 9270  spansnss2t 9415  adjt 9773  nlelch 9909  pjorthco 10008  stge0t 10061  stle1t 10062  stjt 10072  mdsl1 10156  irredlem1 10225  mdsymlem5 10242  fiiu 10350  fiiu2 10377  homcard 10426  filintf 10443  imonclem 10583
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain