Theorem sylan 448

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	⊢ ((φ ⋀ ψ) → χ)
sylan.2	⊢ (θ → φ)

Assertion

Ref	Expression
sylan	⊢ ((θ ⋀ ψ) → χ)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.2	. . 3 ⊢ (θ → φ)
2		sylan.1	. . . 4 ⊢ ((φ ⋀ ψ) → χ)
3	2	ex 373	. . 3 ⊢ (φ → (ψ → χ))
4	1, 3	syl 10	. 2 ⊢ (θ → (ψ → χ))
5	4	imp 350	1 ⊢ ((θ ⋀ ψ) → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  sylanb 449  sylanbr 450  syl2an 454  sylanl1 460  sylanl2 461  syl3an1 858  syl3anl 874  eupick 1432  vtocl2gf 1845  csbnest1g 2033  reuss2 2271  sonr 2854  sotr 2855  so2nr 2857  so3nr 2858  wecmpep 2940  wetrep 2941  wereu 2944  ordelss 2963  ordelord 2969  onelon 2971  ordin 2976  ordtri3or 2978  ordtri3orOLD 2979  ordsssuc 3057  onmindif 3060  ordsucss 3069  ordsucelsuc 3073  ordunisssuc 3083  ordunisuc2 3115  limsssuc 3121  ordom 3141  limom 3146  nnsuc 3148  imadif 3577  fnbr 3593  fnex 3610  feu 3649  fex 3654  dffo2 3677  foco 3684  f1dmex 3712  ffoss 3713  funbrfv 3752  fvco 3776  fvopabg 3787  fvimacnvALT 3811  ffvelrn 3816  dffo4 3822  fopabco 3834  fsn2 3838  fvconst2g 3846  funfvima 3854  funiunfv 3868  f1ocnvfv1 3880  f1ocnvfv2 3881  f1ofveu 3884  f1ocnvfv3 3885  f1ocnvdm 3886  isocnv 3898  isotr 3899  isotrALT 3900  isomin 3901  isoini 3902  isowe 3905  f1oiso 3906  iinon 3912  tfrlem2 3914  tfrlem8 3920  tfrlem11 3923  rdglimt 3950  tz7.48lem 3957  curry1f 4100  oalimcl 4195  oaass 4196  omordi 4198  omword2 4206  omlimcl 4210  odi 4211  omass 4212  oen0 4214  oeordsuc 4222  oelim2 4223  nnaordex 4250  nnawordex 4251  oaabs 4253  ecoprass 4321  mapsn 4346  f1domg 4394  endomtr 4418  fundmen 4426  pw2en 4443  sdomdomtr 4466  mapenlem1 4487  mapenlem2 4488  mapxpen 4493  xpmapenlem4 4497  mapunen 4500  ssenen 4502  phplem1 4506  omsucdom 4520  sucdomi 4521  pssnn 4531  ssfi 4533  isfinite2 4541  unfilem1 4542  unifi 4550  fodomfib 4559  suppr 4582  supsnALT 4584  r1ord 4647  r1val1 4650  rankr1 4666  r1pwcl 4679  rankxplim3 4706  karden 4718  ac6lem 4746  ondomon 4848  ondomcard 4849  alephordi 4866  cardaleph 4877  carduniima 4882  cardinfima 4883  cflim 4901  addclpi 5012  addasspi 5015  mulasspi 5017  addnidpi 5020  ltexpq 5072  prub 5090  genpnnp 5100  genpass 5104  addclprlem1 5110  mulclprlem 5113  1idpr 5125  prlem934b 5130  prlem934 5131  ltexprlem4 5137  ltexprlem6 5139  ltexprlem7 5140  reclem3pr 5150  suplem2pr 5154  00sr 5200  mulgt0sr 5206  recexsr 5208  map2psrpr 5212  suppsr 5214  supsrlem6 5222  supre 5252  adddirt 5311  add4t 5330  cnegextlem3 5339  addsubasst 5375  addsub12t 5378  2addsubt 5381  negcon1t 5402  mul4t 5412  muladd11t 5414  subdirt 5420  negdi2t 5448  negsubdi2t 5450  neg2subt 5451  subsub4t 5456  subadd4t 5467  axsup 5499  eqlet 5564  le2tri3 5583  ltaddsubt 5625  leaddsubt 5627  ltnegcon1t 5649  lenegcon1t 5651  recext 5677  divasst 5724  p1let 5793  ltmul2t 5807  gt0divt 5827  ge0divt 5828  ltdivmult 5839  ledivmult 5840  ltrec1t 5856  lerec2t 5857  ltdiv23t 5860  lediv23t 5861  recgt1it 5868  nn2get 5910  nnltp1let 5922  suprleub 6026  nnunb 6037  xrsupsslem 6043  xrinfmsslem 6044  supxr2 6049  supxrre 6050  supxrunb1 6056  supxrbnd 6058  supxrleub 6066  nn0addclt 6087  elnnz1 6122  zaddclt 6132  elnnnn0b 6140  elnnnn0c 6141  zltp1let 6148  zlem1ltt 6150  gtndivt 6160  primet 6162  msqznn 6163  uzindOLD 6176  btwnz 6183  zmax 6188  zbtwnre 6189  rebtwnz 6190  flltt 6199  fladdzt 6207  ceilet 6213  qaddclt 6227  qrecclt 6231  qdivclt 6232  qbtwnre 6236  seq1rn 6279  seq1cl 6282  seq1cl2 6283  ser1add 6296  shftres 6301  shftval4t 6306  shftcan1t 6311  elioc2t 6342  elico2t 6343  elicc2t 6344  iccsupr 6351  uzss 6383  uzwo2 6409  elfz5t 6426  fzss1t 6455  fzssp1t 6458  fzp1sst 6459  fsequb 6475  fseqsupub 6478  seqzfveq 6506  expgt0t 6540  expgt1t 6543  mulexpt 6545  recexpt 6546  expmult 6548  expordit 6551  expmwordit 6557  exple1t 6558  expubndt 6559  bernneq 6603  expnbndt 6605  sqrlem5 6627  cjexpt 6772  absnidt 6818  absexpt 6823  abssubne0t 6840  absdifltt 6841  absdiflet 6842  lenegsqt 6843  seq1bnd 6867  seq1ublem 6868  cau3ir 6872  cau5i 6874  cvg3 6880  cvganz 6881  facdivt 6899  facndivt 6900  faclbnd3 6904  faclbnd5 6910  faclbnd6 6911  bccmplt 6920  bccl2t 6929  fsump1s 6971  fsumcllem 6972  fsum1ps 6976  fsumsplit 6978  fsumcom 6986  fsumrev 6987  fsumrev2 6988  fsumshftm 6990  fsummulc1 6991  fsumconst 6996  fsumcmpndx2 7000  fsumabs 7001  serz1p 7010  binomlem1 7024  bcxmas 7034  clm3 7037  climrecl 7067  climge0 7069  climaddlem3 7072  climaddc2 7075  climmullem4 7079  climmullem5 7080  climmullem8 7083  clim2serzt 7090  climcmpc1 7095  clim2serz 7101  climabslem 7104  climsup 7111  caucvglem2 7114  caucvglem5 7117  caucvglem6 7118  serzf0 7125  ser1f0 7126  ser1cmp2 7133  isum1p 7161  expcnv 7188  geoisumr 7198  cvgratlem2ALT 7203  cvgratlem5 7209  fsum0diaglem2 7212  fsum0diag2 7214  fsum0diag4 7216  cncffvrn 7228  mulc1cncf 7234  ivthlem7 7242  ivthlem7OLD 7251  efexpt 7334  eftlclt 7341  reeftlclt 7342  abspef01tlub 7356  reeff1o 7388  cos01gt0 7439  demoivre 7446  demoivreALT 7447  ruclem13 7485  infxpidmlem1 7515  infxpidmlem7 7521  infxpidmlem10 7524  infxpidmlem11 7525  infxpidmlem12 7526  infcda 7530  infdif 7531  infmap2lem2 7542  tgss2t 7599  subtop 7608  iscld 7631  clsval 7639  clsval2 7647  clsndisj 7668  neival 7679  ssnei2 7692  opnneiss 7694  lpval 7705  cnco 7730  cnpco 7731  cncnplem4 7739  sncld 7749  metreslem 7786  metxp 7798  bl2in 7807  blssex 7818  ssblex 7820  opni3 7830  opnin 7833  lpbl 7844  metcnpf 7847  metcnplem 7850  metcnp 7851  metcnss 7862  metcnss2 7863  metidcn 7864  lmbr 7892  lmnn 7899  cmscvg 7910  lmss 7916  causs 7918  lmle 7923  lmclim 7926  metelcls 7928  xplmi 7935  xplm 7937  xpcn 7938  oprcn 7939  opr2cn 7941  iscms2lem4 7954  cmsss 7959  bcthlem16 7976  bcthlem17 7977  bcthlem24 7984  bcthlem25 7985  bcthlem30 7990  bcthlem33 7993  grpidinvlem3 8012  grpidinv 8014  grpidinv2 8022  abl23 8068  abl4 8069  ablmuldiv 8072  abldivdiv 8073  abldivdiv4 8074  ablnncan 8077  issubgi 8087  subgabl 8088  ghgrpilem3 8100  ghgrpilem4 8101  ring2 8114  ringaass 8119  ringa23 8120  ringrcan 8122  ringlcan 8123  ring0rid 8125  ring0lid 8126  vcid 8135  vcaass 8145  vca23 8146  vcrcan 8148  vclcan 8149  vc0rid 8151  vc0lid 8152  vcm 8155  vcrinv 8156  vclinv 8157  vcoprnelem 8163  nvass 8209  nvadd23 8211  nvrcan 8212  nvlcan 8213  nvsid 8216  nvsass 8217  nvdi 8219  nvdir 8220  nv2 8221  nv0rid 8224  nv0lid 8225  nv0 8226  nvsz 8227  nvinv 8228  invfval 8229  nvnnncan1 8236  nvnnncan2 8237  nvnegneg 8239  nvrinv 8241  nvlinv 8242  nvaddsubass 8246  nvaddsub 8247  nvcl 8255  nvmtri2 8268  nvelbl 8292  nvelbl2 8293  nvlmcl 8296  ipid 8326  sspg 8350  ssps 8352  sspmval 8355  sspn 8358  sspival 8360  sspimsval 8362  lnosub 8382  lnomul 8383  nvcnpi4 8384  nmoub3i 8397  nmounbi 8400  blometi 8423  ipasslem1 8450  ipasslem2 8451  ipasslem3 8452  ipasslem4 8453  ipasslem5 8454  ipasslem8 8457  ipdi 8463  ipassr 8466  ipsubdir 8468  ipsubdi 8469  sspph 8475  ubthlem3 8491  ubthlem5 8493  ubthlem6 8494  ubthlem9 8497  ubthlem10 8498  ubthlem11 8499  minveclem9 8513  minveclem25 8529  minveclem27 8531  minveclem28 8532  minveclem38 8542  hlass 8562  hladdid 8564  hlmulid 8566  hlmulass 8567  hldi 8568  hldir 8569  hlmul0 8570  hlipdir 8573  hlipass 8574  hlcompl 8576  htthlem5 8583  htthlem6 8584  htthlem8 8586  htthlem10 8588  pstr 8610  efif1lem5 8684  circgrpOLD 8693  shftefif1olem 8696  shftefif1olemOLD 8697  explogt 8729  reexplogt 8730  relogexpt 8731  logexptOLD 8747  explogtOLD 8748  axgroth3 8753  h2hlm 8824  hvadd4t 8879  hvaddsubasst 8884  hvmulcan2t 8914  hiassdit 8931  hcau2 9029  hlim2 9034  hhcms 9046  hsn0elch 9094  norm1ex 9096  hhssnv 9108  hhsscms 9124  ocsh 9130  occllem6 9152  projlem21 9180  projlem25 9184  projlem26 9185  pjpjtht 9231  pjopt 9233  pjpot 9234  pjocclt 9239  shsel3t 9252  elspanclt 9278  chsscon1t 9397  chpsscon1t 9400  chdmm2t 9422  chdmj2t 9426  h1de2ctlem 9452  elspansnclt 9462  pjspansnt 9475  fh2t 9537  cm2jt 9538  osumlem1 9553  osumlem2 9554  spansncv 9572  5oalem2 9575  3oalem1 9582  pjot 9591  pjjs 9620  pjds 9632  pjds3 9633  pjoi0t 9637  hoadd4t 9685  homco1t 9702  homulasst 9703  hoadddit 9704  hoadddirt 9705  honegsubdi2t 9712  hosubadd4t 9715  hoaddsubasst 9716  hosubsub4t 9719  adjsymt 9734  cnvadj 9791  hhlno 9801  unopf1ot 9814  unopnormt 9815  cnvunopt 9816  unopadjt 9817  unoplint 9818  counopt 9819  hmopret 9821  adjclt 9830  adj2t 9832  hmoplint 9840  braclt 9847  kbopt 9851  kbmult 9853  eighmret 9861  eighmortht 9862  lnopmult 9865  lnopmulsub 9874  0lnfn 9883  lnopm 9898  lnophs 9899  lnopco 9901  nmopunt 9912  hmopst 9918  hmopmt 9919  hmopcot 9921  nmcopexlem3 9926  nmcopexlem5 9928  nmcopexlem6 9929  lnopcon 9936  nmcfnexlem3 9955  nmcfnexlem5 9957  nmcfnexlem6 9958  lnfncon 9963  nlelch 9967  riesz3 9968  cnlnadjlem2 9974  cnlnadjlem6 9978  cnlnadjlem7 9979  cnlnadjeu 9983  adjbdlnt 9989  adjlnopt 9992  adjmult 9998  adjaddt 9999  nmopco 10001  adjco 10006  nmopcoadj 10007  branmfnt 10011  cnvbramult 10021  kbass2t 10023  kbass5t 10026  leop2t 10030  leopsqt 10035  leopaddt 10038  leopmulit 10039  leopmult 10040  leopnmidt 10044  nmopleidt 10045  pjnmop 10048  hmopidmchlem 10051  hmopidmch 10052  pjadjco 10062  pjima 10077  pjadj2co 10105  stclt 10116  hstclt 10117  stadd 10146  strlem3 10153  strlem4 10154  strlem5 10155  hstrlem3 10161  hstrlem4 10162  hstrlem5 10163  cvcon3t 10184  mdbr2 10196  dmdmdt 10200  mddmd 10207  mdsl0 10208  mdsl3t 10214  mdslmd1lem1 10223  mdslmd4 10231  atsseq 10245  atcveq0 10246  ch1dle 10250  atom1d 10251  superpos 10252  shatomic 10256  shatomistic 10259  cvexchlem 10266  atnem0 10275  atcv0eq 10277  atord 10282  atcvatlem 10283  irredlem1 10288  irredlem2 10289  irredlem3 10290  atcvat3 10294  atdmd 10296  mdsymlem5 10305  sumdmdlem 10315  cdj3lem2 10330  symggrpiOLD 10374  symggrpi 10376  cayleylem2 10380  idmoa 10580  rcmob 10598  idosc 10618  dmo 10625  cdmo 10626  jdmo 10627  homib 10640  iri 10644

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