Theorem 3syl 20

Description: Inference chaining two syllogisms.

Hypotheses

Ref	Expression
3syl.1	|- (ph -> ps)
3syl.2	|- (ps -> ch)
3syl.3	|- (ch -> th)

Assertion

Ref	Expression
3syl	|- (ph -> th)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- (ph -> ps)
2		3syl.2	. . 3 |- (ps -> ch)
3	1, 2	syl 10	. 2 |- (ph -> ch)
4		3syl.3	. 2 |- (ch -> th)
5	3, 4	syl 10	1 |- (ph -> th)

Syntax hints:   -> wi 3

This theorem is referenced by:  nicodraw 950  ax5o 972  ax67to6 1019  ax467 1021  ax467to6 1023  19.9d 1035  hbs1f 1187  aev 1206  hbsb4 1246  dvelimdf 1249  sbcom 1256  a12stdy3 1372  mo 1391  eupickb 1433  euor2 1435  2mo 1445  2eu2 1448  hbabd 1466  rgen2a 1696  hbsbc1gd 1979  hbsbcgd 1980  npss0 2305  iununi 2611  opthwiener 2802  elpwunsn 2907  onin 2973  ssorduni 2988  onelsst 2995  onssneli 3096  onuninsuc 3103  limsuc 3115  xpexg 3254  dmsnop 3323  dmexg 3352  rnexg 3353  relfld 3507  unixp0 3510  fununi 3555  resfunexg 3571  fn0 3597  fssxp 3628  fabexg 3644  foima 3667  f1imacnv 3696  f1ococnv2 3699  f1dmex 3701  fo00 3706  fvres 3725  cbvfo 3876  isomin 3890  isoini 3891  isofrlem 3892  isowe 3894  canth 3898  tfrlem10 3911  tfrlem11 3912  tfrlem13 3914  tz7.44-2 3920  tz7.44-3 3921  rdglem2 3929  hboprd 3973  1stcof 4091  eloprabi 4108  omv 4141  oev 4143  oe1m 4169  oaord 4171  oawordeulem 4178  oalimcl 4184  oarec 4186  om00 4196  oen0 4203  oelim2 4212  nnacom 4223  oaabs 4242  qsexg 4284  eceqopreq 4303  map0 4334  f1imaen 4409  en1 4413  xpdom3 4431  sbthlem1 4433  sbthlem2 4434  sbth 4443  mapenlem2 4476  phplem4 4497  php3 4501  php4 4502  0sdom1dom 4510  ssnn 4520  unblem1 4523  unfilem1 4530  unifi 4538  fiint 4540  fodomfi 4546  inf3lem7 4599  tz9.12lem3 4641  r1val3 4659  rankxplim2 4693  rankxplim3 4694  rankxpsuc 4695  scott0 4697  aceq5lem4 4718  ac6lem 4734  numthlem 4763  numth 4764  zorn2lem2 4769  zorn2lem7 4774  fodom 4778  brdom3 4781  brdom5 4782  brdom4 4783  oncard 4809  sucdom 4822  unxpdomlem 4823  sucxpdom 4826  cardlim 4831  ondomon 4836  carduni 4838  cardaleph 4865  iscard3 4868  alephfp 4880  dominf 4884  cdadom2 4914  nd3 4920  mulidpi 4994  ltsopi 4996  mulcanpi 5007  enqeceq 5027  addclpq 5038  mulclpq 5040  1qec 5048  ltapq 5056  halfpq 5062  prnmadd 5080  addclprlem2 5099  1idpr 5113  prlem934a 5117  prlem934 5119  ltaddpr 5120  ltexprlem3 5124  ltexprlem4 5125  ltexprlem6 5127  prlem936a 5133  prlem936 5135  reclem1pr 5136  suplem2pr 5142  enreceq 5157  addclsr 5172  mulclsr 5173  suppsr 5202  suppsr2 5203  supsrlem2 5206  ltpnft 5523  mnfltt 5524  ledivp1 5862  ltdivp1 5863  nnleltp1t 5909  lbcl 6001  lbinfm 6003  infmrcl 6024  supxr 6036  supxrre1 6048  supxrre2 6049  nn0ltp1let 6082  zeot 6154  uzwo3lem2 6173  zbtwnre 6177  flget 6186  flidt 6188  fladdzt 6195  flhalft 6197  ceiclt 6198  ceiget 6199  ceim1lt 6200  ceilet 6201  zqt 6206  qbtwnre 6224  om2uzlt 6243  om2uzf1o 6246  uzrdgsuc 6249  seq1val 6257  icoshftf1oi 6350  peano2uzr 6388  eluzfz2t 6429  elfzp1 6450  fzneuzt 6458  seq1seq02t 6483  seqzp1 6488  seq0p1 6491  sumsqne0 6573  discrlem2 6595  discrlem3 6596  nnesq 6600  sqrlem12 6622  recjt 6761  absdivz 6802  releabst 6832  cjdiv 6834  seq1bnd 6855  facwordit 6889  faclbnd 6890  faclbnd2 6891  faclbnd4lem3 6895  faclbnd6 6899  facavgt 6900  bccmplt 6908  bcpasc 6915  fsum1 6951  fsump1 6952  fsum3 6970  fsum4 6971  fsumrev 6975  fsum0 6985  ser1ser0 6994  binomlem1 7012  binomlem2 7013  binomlem3 7014  binomlem4 7015  binomlem5 7016  bcxmas 7022  climunii 7043  climshft 7049  climrecl 7055  climge0 7057  climaddlem3 7060  climcmplem 7081  climabslem 7092  climcj 7094  climsup 7099  fnsmntlem 7168  fnsmnt 7169  cvgratlem2ALT 7191  cvgratlem4 7196  abscncflem 7217  cjcncf 7221  dsupivthlem 7234  efcltlem1 7254  efaddlem2 7289  efaddlem5 7292  efaddlem6 7293  efaddlem13 7300  efaddlem14 7301  efaddlem16 7303  efaddlem17 7304  efne0t 7319  eftabs 7325  ef01tllem2 7334  eirrlem2 7339  efgt0 7353  absefm1le 7360  efcnlem4 7370  efcn 7371  sinclt 7381  cosclt 7382  sin01bndlem2 7418  cos01bndlem2 7420  sin02gt0 7428  abseft 7433  demoivre 7434  znnen 7453  infxpidmlem11 7513  infdif 7519  infxp 7523  infmap1 7524  infmap2 7531  alephexp2 7536  tgvalt 7566  cctop 7602  ntrfval 7617  clsfval 7618  neifval 7664  lpfval 7692  cnpfval 7707  cnpco 7719  iscncl 7720  ismet 7748  dfms2 7749  meteq0 7762  metne0 7773  metres 7775  blfval 7787  metcnss 7850  metcnss2 7851  lmfval 7877  caufval 7878  caun0 7896  lmle 7911  bcthlem33 7981  grpidval 8008  grpinvval 8017  resgrprn 8045  resgrprnOLD 8046  issubg 8068  subgres 8069  ringid 8097  ring2 8101  nvgf 8189  nvs 8242  nvz 8249  imsba 8272  ipcl 8312  ip1cnilem1 8320  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem4 8323  ip1cnilem5 8324  sspba 8333  sspg 8334  ssps 8336  sspmlem 8338  sspn 8342  sspival 8344  nmogtmnf 8378  nmblore 8391  0oo 8394  phop 8421  cnph 8422  pilem1 8609  sinperlem2 8625  sinmpi 8632  cosmpi 8633  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  cosh111lem1 8648  efif 8655  efifolem6 8661  efif1lem3 8666  efif1lem4 8667  efielcircOLD 8674  efielcirc 8678  eff1i 8683  effoi 8684  efper 8686  hhph 8984  hlimunii 9047  occllem6 9117  projlem1 9125  projlem8 9132  projlem10 9134  projlem12 9136  projlem13 9137  projlem15 9139  projlem24 9148  projlem25 9149  projlem26 9150  pjthlem2 9158  pjthlem7 9163  pjthlem8 9164  dfch2 9187  ococint 9235  spanssoc 9257  spansncht 9422  osumlem3 9520  osumlem5 9522  5oalem5 9543  pjige0 9575  pjocin 9583  eigre 9700  nmopgtmnf 9735  nmopret 9737  nmopge0t 9774  unopadjt 9782  unoplint 9783  nmfnge0t 9790  adjadjt 9799  unopadj2t 9801  eigvalclt 9824  hmopidmchlem 10016  pjsspos 10038  pjclem4 10065  pj2cocl 10071  pj3s 10073  hstlest 10096  strlem1 10115  strlem3a 10117  strlem5 10120  strlem6 10121  hstrlem6 10129  h1dat 10213  atom1d 10217  shatomistic 10225  atoml 10246  mdsymlem1 10267  mdsymlem3 10269  mdsym 10275  sumdmdlem 10281  dmdbr5at 10284  ghomfo 10325  ghomcl 10326  cayleylem2 10344  cayleylem3 10345  f2imacnv 10406  mapdiscn 10434  cmphmp 10444  idhme 10445  hmeogrp 10461  qusp 10466  fgsb 10480  dtt2 10498  mslb1 10509  2wsms 10510  msra3 10511  iintlem1 10512  isalg 10533  algi 10540  rdmob 10561  rcmob 10562  domc 10578  codc 10579  idc 10580  cmppfc 10581  cmpmorp 10592  mrdmcd 10602  eqidob 10603  homib 10604  ismonc 10620  hgrablkne0 10645

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain