Theorem syldan 467

Description: A syllogism deduction with conjoined antecents.

Hypotheses

Ref	Expression
syldan.1	|- ((ph /\ ps) -> ch)
syldan.2	|- ((ph /\ ch) -> th)

Assertion

Ref	Expression
syldan	|- ((ph /\ ps) -> th)

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 373	. . 3 |- (ph -> (ps -> ch))
3		syldan.2	. . . 4 |- ((ph /\ ch) -> th)
4	3	ex 373	. . 3 |- (ph -> (ch -> th))
5	2, 4	syld 27	. 2 |- (ph -> (ps -> th))
6	5	imp 350	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  csbnest1g 2033  elpw2g 2722  mouniss 2885  elpwunsn 2907  fnbr 3582  fnex 3599  tfr3 3917  tz7.48-2 3948  omlimcl 4199  ixpexg 4348  fofi 4548  iunfi 4549  ltaddpr 5120  ltexprlem7 5128  1idsr 5187  addgt0sr 5193  pm2.61ltle 5515  mulgt1t 5809  lediv1t 5814  gt0divt 5815  ge0divt 5816  lemuldivt 5832  ltrec1t 5844  lerec2t 5845  lediv2t 5847  ltdiv23t 5848  lediv23t 5849  lediv12it 5852  recrecltt 5858  nn2get 5898  lbinfm 6003  xrsupsslem 6031  xrinfmsslem 6032  supxr 6036  supxr2 6037  supxrpnf 6043  supxrunb1 6044  supxrunb2 6045  recnzt 6146  uzwo2 6397  fznn0sub2t 6439  expord2t 6543  exple1t 6546  le2sqit 6571  expnbndt 6593  leabst 6807  faclbnd4lem3 6895  bcval4t 6907  fsum1s2 6956  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumrev 6975  fsummulc1 6979  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  climconst 7039  climaddc2 7063  climmullem5 7068  climmullem8 7071  clim2serzt 7078  clim2serz 7089  iserzex 7090  isumclim3t 7143  isumclim5t 7145  isum1p 7149  isumreclt 7153  georeclim 7183  geoisumr 7186  cvgratlem5 7197  fsum0diaglem2 7200  cncffvrn 7216  efaddlem6 7293  reeff1o 7376  unbenlem 7455  infdif 7519  tgclt 7574  basgen2t 7589  opncld 7624  iincld 7629  uncld 7631  ntrval2 7636  clsss3 7641  ntrss3 7642  clsidm 7648  ntridm 7649  opnssneib 7679  ssnei2 7680  neindisj 7681  innei 7686  dnsconst 7738  metxptval 7782  ssblex 7808  opni2 7817  metcn 7841  metcnpi3 7844  metcnpi4 7845  cncfmet 7857  lmnn 7887  lmsslem 7903  metelcls 7916  cmsss 7947  bcthlem21 7969  grpidinvlem2 7999  grpidinvlem3 8000  grpideu 8003  grpinvid1 8022  grpinvid2 8023  grplcan 8025  grp2inv 8028  grpinvop 8030  grpmuldivass 8038  grppnpcan2 8042  grpnnncan2 8043  grpnpncan 8044  grplactf1o 8049  abl4 8056  ablmuldiv 8059  abldivdiv4 8061  ablnnncan 8063  ablnnncan1 8065  ghgrpilem3 8087  vc0 8140  vcz 8141  nvzs 8217  nvmdi 8222  nvnegneg 8223  nvsubadd 8227  nvnpcan 8232  nvmeq0 8236  nvabs 8253  nvlmle 8281  sspmval 8339  sspz 8341  sspival 8344  sspimsval 8346  lnosub 8366  lnomul 8367  nmoub3i 8381  0lno 8395  nmblolbii 8403  blocnilem 8408  blocni 8409  ipsubdir 8452  sspph 8459  ubthlem9 8481  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  pstr 8594  efifolem7 8662  hvaddsub4t 8884  hi2eqt 8910  chocuni 9111  projlem26 9150  shsel3t 9217  chabs1t 9377  pjspansnt 9440  5oalem2 9540  3oalem2 9548  pjoi0t 9602  nmopub2tALT 9773  nmfnleub2t 9789  elnlfn2t 9792  eigvalclt 9824  eighmret 9826  leopmult 10005  nmopleidt 10010  spansncv2t 10158  chcv1t 10219  atcv0eq 10243  atexcht 10245  irred 10258  cdj1 10294  lediv2itALT 10305  ghomf1olem 10330  findabrcl 10352  qusp 10466  msr4 10506

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain