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

Theorem syl3an3 1219
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 1152 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 65 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1147 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl3an3b  1222  syl3an3br  1225  vtoclgft  2962  disji  4160  ovmpt2x  6161  ovmpt2ga  6162  unbnn2  7323  axdc3lem4  8289  axdclem2  8356  gruiin  8641  gruen  8643  divass  9652  ltmul2  9817  xleadd1  10790  xltadd2  10792  xlemul1  10825  xltmul2  10828  elfzo  11097  modcyc2  11232  faclbnd5  11544  subcn2  12343  mulcn2  12344  ndvdsp1  12884  gcddiv  13004  lubel  14504  oddvdsi  15141  odcong  15142  odeq  15143  efgsp1  15324  lspsnss  16021  iuncld  17064  neips  17132  opnneip  17138  hmeof1o2  17748  ordthmeo  17787  ufinffr  17914  elfm3  17935  utop3cls  18234  blcntrps  18395  blcntr  18396  neibl  18484  blnei  18485  metss  18491  stdbdmetval  18497  prdsms  18514  blval2  18558  lmmbr  19164  lmmbr2  19165  iscau2  19183  bcthlem1  19230  bcthlem3  19232  bcthlem4  19233  dvn2bss  19769  dvfsumrlim  19868  dvfsumrlim2  19869  cxpexpz  20511  cxpsub  20526  2pthon  21555  gxpval  21800  gxnn0neg  21804  gxnn0suc  21805  gxcl  21806  gxneg  21807  gxcom  21810  gxinv  21811  gxsuc  21813  gxnn0add  21815  gxadd  21816  gxsub  21817  gxnn0mul  21818  gxmul  21819  hvaddsub12  22493  hvaddsubass  22496  hvsubdistr1  22504  hvsubcan  22529  hhssnv  22717  spanunsni  23034  homco1  23257  homulass  23258  hoadddir  23260  hosubdi  23264  hoaddsubass  23271  hosubsub4  23274  lnopmi  23456  adjlnop  23542  mdsymlem5  23863  disjif  23973  disjif2  23976  ind0  24370  sigaclfu  24455  wfrlem14  25483  clsint2  26222  comppfsc  26277  isbnd2  26382  blbnd  26386  isdrngo2  26464  jm2.22  26956  jm2.23  26957  lindsmm2  27167  dvconstbi  27419  eelT11  28520  eelT12  28524  eelTT1  28526  eelT01  28527  eel0T1  28528  bnj544  28971  bnj561  28980  bnj562  28981  bnj594  28989  atnem0  29801  hlrelat5N  29883  ltrnel  30621  ltrnat  30622  ltrncnvat  30623
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator