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

Theorem syl3an3 1253
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 1186 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 68 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1181 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  syl3an3b  1256  syl3an3br  1259  vtoclgft  3041  disji  4301  ovmpt2x  6240  ovmpt2ga  6241  unbnn2  7590  axdc3lem4  8643  axdclem2  8710  gruiin  8998  gruen  9000  divass  10033  ltmul2  10201  xleadd1  11239  xltadd2  11241  xlemul1  11274  xltmul2  11277  elfzo  11576  modcyc2  11765  faclbnd5  12095  subcn2  13093  mulcn2  13094  ndvdsp1  13634  gcddiv  13754  lubel  15313  gsumccatsn  15542  oddvdsi  16072  odcong  16073  odeq  16074  efgsp1  16255  lspsnss  17093  lindsmm2  18280  mulmarep1el  18405  mdetunilem4  18443  iuncld  18671  neips  18739  opnneip  18745  hmeof1o2  19358  ordthmeo  19397  ufinffr  19524  elfm3  19545  utop3cls  19848  blcntrps  20009  blcntr  20010  neibl  20098  blnei  20099  metss  20105  stdbdmetval  20111  prdsms  20128  blval2  20172  lmmbr  20791  lmmbr2  20792  iscau2  20810  bcthlem1  20857  bcthlem3  20859  bcthlem4  20860  dvn2bss  21426  dvfsumrlim  21525  dvfsumrlim2  21526  cxpexpz  22134  cxpsub  22149  2pthon  23523  gxpval  23768  gxnn0neg  23772  gxnn0suc  23773  gxcl  23774  gxneg  23775  gxcom  23778  gxinv  23779  gxsuc  23781  gxnn0add  23783  gxadd  23784  gxsub  23785  gxnn0mul  23786  gxmul  23787  hvaddsub12  24462  hvaddsubass  24465  hvsubdistr1  24473  hvsubcan  24498  hhssnv  24687  spanunsni  25004  homco1  25227  homulass  25228  hoadddir  25230  hosubdi  25234  hoaddsubass  25241  hosubsub4  25244  lnopmi  25426  adjlnop  25512  mdsymlem5  25833  disjif  25944  disjif2  25947  ind0  26498  sigaclfu  26584  wfrlem14  27759  ftc1anclem6  28498  clsint2  28550  comppfsc  28605  isbnd2  28708  blbnd  28712  isdrngo2  28790  jm2.22  29370  jm2.23  29371  dvconstbi  29634  wlkcompim  30313  wwlknext  30382  clwlkcompim  30453  clwwlkel  30481  clwwlkf  30482  wwlkextproplem3  30588  numclwlk1lem2f1  30713  rmfsupp  30818  mndpfsupp  30820  scmfsupp  30822  eelT11  31528  eelT12  31532  eelTT1  31534  eelT01  31535  eel0T1  31536  bnj544  31983  bnj561  31992  bnj562  31993  bnj594  32001  atnem0  33059  hlrelat5N  33141  ltrnel  33879  ltrnat  33880  ltrncnvat  33881
  Copyright terms: Public domain W3C validator