MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an3 Unicode version

Theorem syl3an3 1217
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1  |-  ( ph  ->  th )
syl3an3.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an3  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3  |-  ( ph  ->  th )
2 syl3an3.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1150 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 63 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1145 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3an3b  1220  syl3an3br  1223  vtoclgft  2847  disji  4027  ovmpt2x  5992  ovmpt2ga  5993  unbnn2  7130  axdc3lem4  8095  axdclem2  8163  gruiin  8448  gruen  8450  divass  9458  ltmul2  9623  xleadd1  10591  xltadd2  10593  xlemul1  10626  xltmul2  10629  elfzo  10893  modcyc2  11016  faclbnd5  11327  subcn2  12084  mulcn2  12085  ndvdsp1  12624  gcddiv  12744  lubel  14242  oddvdsi  14879  odcong  14880  odeq  14881  efgsp1  15062  lspsnss  15763  iuncld  16798  neips  16866  opnneip  16872  hmeof1o2  17470  ordthmeo  17509  ufinffr  17640  elfm3  17661  blcntr  17980  neibl  18063  blnei  18064  metss  18070  stdbdmetval  18076  prdsms  18093  lmmbr  18700  lmmbr2  18701  iscau2  18719  bcthlem1  18762  bcthlem3  18764  bcthlem4  18765  dvn2bss  19295  dvfsumrlim  19394  dvfsumrlim2  19395  cxpexpz  20030  cxpsub  20045  gxpval  20942  gxnn0neg  20946  gxnn0suc  20947  gxcl  20948  gxneg  20949  gxcom  20952  gxinv  20953  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxsub  20959  gxnn0mul  20960  gxmul  20961  hvaddsub12  21633  hvaddsubass  21636  hvsubdistr1  21644  hvsubcan  21669  hhssnv  21857  spanunsni  22174  homco1  22397  homulass  22398  hoadddir  22400  hosubdi  22404  hoaddsubass  22411  hosubsub4  22414  lnopmi  22596  adjlnop  22682  mdsymlem5  23003  disjif  23370  disjif2  23373  sigaclfu  23495  wfrlem14  24340  sndw2  25204  tartarmap  25991  clsint2  26350  comppfsc  26410  isbnd2  26610  blbnd  26614  isdrngo2  26692  jm2.22  27191  jm2.23  27192  lindsmm2  27402  dvconstbi  27654  eelT11  28788  eelT12  28792  eelTT1  28794  eelT01  28795  eel0T1  28796  bnj544  29242  bnj561  29251  bnj562  29252  bnj594  29260  atnem0  30130  hlrelat5N  30212  ltrnel  30950  ltrnat  30951  ltrncnvat  30952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator