MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an3 Structured version   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  2994  disji  4192  ovmpt2x  6194  ovmpt2ga  6195  unbnn2  7356  axdc3lem4  8325  axdclem2  8392  gruiin  8677  gruen  8679  divass  9688  ltmul2  9853  xleadd1  10826  xltadd2  10828  xlemul1  10861  xltmul2  10864  elfzo  11134  modcyc2  11269  faclbnd5  11581  subcn2  12380  mulcn2  12381  ndvdsp1  12921  gcddiv  13041  lubel  14541  oddvdsi  15178  odcong  15179  odeq  15180  efgsp1  15361  lspsnss  16058  iuncld  17101  neips  17169  opnneip  17175  hmeof1o2  17787  ordthmeo  17826  ufinffr  17953  elfm3  17974  utop3cls  18273  blcntrps  18434  blcntr  18435  neibl  18523  blnei  18524  metss  18530  stdbdmetval  18536  prdsms  18553  blval2  18597  lmmbr  19203  lmmbr2  19204  iscau2  19222  bcthlem1  19269  bcthlem3  19271  bcthlem4  19272  dvn2bss  19808  dvfsumrlim  19907  dvfsumrlim2  19908  cxpexpz  20550  cxpsub  20565  2pthon  21594  gxpval  21839  gxnn0neg  21843  gxnn0suc  21844  gxcl  21845  gxneg  21846  gxcom  21849  gxinv  21850  gxsuc  21852  gxnn0add  21854  gxadd  21855  gxsub  21856  gxnn0mul  21857  gxmul  21858  hvaddsub12  22532  hvaddsubass  22535  hvsubdistr1  22543  hvsubcan  22568  hhssnv  22756  spanunsni  23073  homco1  23296  homulass  23297  hoadddir  23299  hosubdi  23303  hoaddsubass  23310  hosubsub4  23313  lnopmi  23495  adjlnop  23581  mdsymlem5  23902  disjif  24012  disjif2  24015  ind0  24409  sigaclfu  24494  wfrlem14  25543  ftc1anclem6  26275  clsint2  26323  comppfsc  26378  isbnd2  26483  blbnd  26487  isdrngo2  26565  jm2.22  27057  jm2.23  27058  lindsmm2  27267  dvconstbi  27519  eelT11  28748  eelT12  28752  eelTT1  28754  eelT01  28755  eel0T1  28756  bnj544  29202  bnj561  29211  bnj562  29212  bnj594  29220  atnem0  30053  hlrelat5N  30135  ltrnel  30873  ltrnat  30874  ltrncnvat  30875
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