Theorem sylan2 451

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2	⊢ ((φ ⋀ θ) → χ)

Proof of Theorem sylan2

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

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  sylan2b 452  sylan2br 453  syl2an 454  sylanr1 462  sylanr2 463  ax11indalem 1366  ax11inda2ALT 1367  elabgt 1891  sbciegft 1955  hbsbc1gd 1979  hbsbcgd 1980  hbcsb1gd 2023  hbcsbgd 2024  csbnestg 2032  sbcnestg 2034  sspr 2471  ssiun 2587  uniexb 2902  trssord 2960  ordelssne 2969  onint 3001  onint0 3002  onnmin 3010  onsssuc 3053  onsucmin 3067  ordsucun 3077  nlimsucg 3107  ordunisuc2 3110  peano5 3148  findsg 3152  tfindsg 3157  tfindsg2 3158  cnvexg 3511  coexg 3516  funimass2 3565  cofunexg 3572  cofunex2g 3573  dmfex 3646  funbrfv 3741  eqfnfv 3788  fvimacnvi 3795  fvimacnvALT 3800  funiunfv 3857  isofrlem 3892  tfrlem8 3909  tfrlem9 3910  tfrlem11 3912  tfr3 3917  foprrn 4026  fnoprvalrn 4029  oasuc 4153  omsuc 4155  oalim 4157  omlim 4158  oalimcl 4184  oaass 4185  omlimcl 4199  odi 4200  omass 4201  oneo 4202  oelim2 4212  nnaordex 4239  nnawordex 4240  oaabslem 4241  ecoprass 4310  ecoprdi 4311  mapex 4318  f1oen2g 4381  f1oeng 4382  domentr 4408  undom 4424  pwuninel 4472  mapunen 4488  ssenen 4490  phplem3 4496  phplem4 4497  php 4499  php3 4501  onomeneq 4504  omsucdom 4508  ssfi 4521  unbnn2 4528  unfi 4534  unifi 4538  fodomfi 4546  iunfi 4549  pm54.43 4552  supmaxlem 4568  omex 4607  aceq3 4713  aceq5 4720  aceq6b 4722  ac5b 4733  zorn2lem3 4770  imadomg 4786  sucdom 4822  ondomon 4836  alephnbtwn 4848  alephordi 4854  alephval2 4882  cfom 4896  axrepndlem2 4925  axpowndlem4 4932  axinfndlem1 4937  axacndlem5 4943  addclpi 5000  addasspi 5003  mulasspi 5005  distrpi 5006  mulcanpi 5007  indpi 5014  ltapq 5056  ltrpq 5065  prcdpq 5077  genpass 5092  distrlem1pr 5107  distrlem2pr 5108  distrlem4pr 5110  psslinpr 5115  prlem934b 5118  ltexprlem6 5127  ltexprlem7 5128  prlem936b 5134  prlem936 5135  reclem3pr 5138  reclem4pr 5139  recexsrlem 5192  suppsr3 5204  pre-axsup 5271  cnegextlem1 5325  cnegextlem3 5327  cnegext 5328  subnegt 5374  subdit 5407  1re 5415  resubclt 5418  mulneg2t 5432  negsubdit 5437  submul2t 5440  subsub2t 5441  nnncan1t 5447  addsub4t 5453  xrret 5550  le2tri3 5571  ltaddsubt 5613  leaddsubt 5615  lenegcon2t 5640  recextlem1 5663  recextlem2 5664  recext 5665  divnegt 5738  letrp1t 5780  lerec2t 5845  ledivdivt 5846  lediv12it 5852  ledivp1t 5861  nndivt 5914  nndivtrt 5915  lble 6002  sup2 6006  dfinfmr 6022  nnunb 6025  arch 6026  bndndx 6028  xrsupsslem 6031  xrinfmsslem 6032  supxrunb1 6044  nn0ge0t 6072  nn0addclt 6075  nn0leltp1t 6083  nn0addge1t 6085  nn0addge2t 6086  zaddclt 6120  zsubclt 6123  zrevaddclt 6125  elnn0nn 6126  zltp1let 6136  zleltp1t 6137  zltlem1t 6139  peano2uz2 6157  uzind 6161  uzindOLD 6164  uzwo4OLD 6166  uzwo3lem1 6172  zmax 6176  zbtwnre 6177  rebtwnz 6178  flget 6186  flwordit 6191  flbit 6192  fladdzt 6195  qaddclt 6215  qsubclt 6218  qrecclt 6219  qdivclt 6220  qrevaddclt 6221  qbtwnre 6224  qsqueeze 6226  seq1rn2 6266  ser1recl 6276  elioc2t 6330  elico2t 6331  elicc2t 6332  icounlem 6353  eluzp1lt 6374  uzwo 6395  uzwoOLD 6396  fzss2t 6444  fzrev2t 6452  fzrev3it 6455  fzrevralt 6459  fsequb 6463  fsequb2 6464  fseqsupub 6466  seqzp1 6488  seqzval2t 6493  seqzeq 6495  seqzrn2 6496  seqzrn 6497  ser0cl1 6504  expnnvalt 6512  expp1t 6514  expm1t 6523  expeq0t 6525  expge0t 6530  expgt1t 6531  expge1t 6532  bernneq 6591  replimt 6700  resubt 6749  imsubt 6752  cjsubt 6759  sqabsaddt 6791  sqabssubt 6792  seq1bnd 6855  cau3ir 6860  cau5i 6862  cvg2 6867  facclt 6885  facdivt 6887  faclbnd4lem3 6895  faclbnd4lem4 6896  faclbnd5 6898  bccmplt 6908  fsum1s 6955  fsump1s 6959  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsumshft 6977  fsummulc1 6979  fsummulc2 6980  fsum2mul 6983  fsumconst 6984  fsumcmp 6986  fsumcmp0 6987  fsumcmpndx2 6988  fsumabs 6989  fsumabs2mul 6990  serzcl2t 6995  serzcmp0 7001  binomlem1 7012  binomlem2 7013  binomlem5 7016  binomlem6 7017  clm4 7026  clm4le 7027  clm4f 7028  clm4at 7036  climfnn 7038  2climnn 7047  2climnn0 7048  iserzshft2 7052  climge0 7057  climaddlem3 7060  climaddc1 7062  climmullem3 7066  climmullem5 7068  climmullem8 7071  climmulc2 7073  climsubc2 7075  clim2serzt 7078  iserzmulc1 7080  iserzcmp 7086  clim2serz 7089  climserzle 7091  climsup 7099  caucvglem6 7106  isumreclt 7153  expcnv 7176  geoisum1c 7188  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem2 7194  cvgratlem4 7196  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202  mulc1cncf 7222  ivthlem7 7230  ivthlem7OLD 7239  efcltlem1 7254  erelem1 7269  erelem3 7271  efaddlem5 7292  efaddlem6 7293  efsubt 7321  efexpt 7322  reeftlclt 7330  sinsubt 7405  cossubt 7406  demoivreALT 7435  acdc5lem1 7441  acdcALT 7446  znnenlem 7451  znnenlemOLD 7452  unbenlem 7455  ruclem13 7473  infxpidmlem1 7503  infxpidmlem8 7510  infxpidmlem11 7513  infxpidmlem12 7514  infdif 7519  iunopnt 7549  istps3 7558  eltgt 7568  eltg2t 7569  tgclt 7574  tgval3t 7575  basgen2t 7589  bastop 7592  subbas2 7595  fctop 7600  clsval2 7635  ntrss 7638  isnei 7668  isneip 7670  neips 7677  islp2 7697  iscncl 7720  metreslem 7774  blin 7804  blss 7805  isopn4 7814  opnin 7821  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnss 7850  metcnss2 7851  lmbr 7880  lmnn 7887  lmuni 7902  causs 7906  lmfexlem2 7908  metelcls 7916  metcnp4 7920  xplmi2 7924  opr1cn 7928  lmcau 7946  bcthlem1 7949  bcthlem9 7957  bcthlem10 7958  bcthlem14 7962  bcthlem16 7964  bcthlem21 7969  grpidinvlem1 7998  grpidinvlem2 7999  grpideu 8003  resgrprn 8045  grplactfval 8047  ablnncan 8064  issubgi 8074  ablmul 8083  ghgrpilem4 8088  isvc 8152  isnv 8183  nvmul0or 8224  imsmetlem 8274  nvlmle 8281  nmcnilem 8285  sm1cnilem 8294  ipcl 8312  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem5 8324  ip1cnilem6 8325  sspival 8344  lnocoi 8365  nmosetre 8372  nmoge0 8375  nmoub3i 8381  nmobndi 8383  nmlno0lem 8398  blo3i 8406  blometi 8407  blocnilem 8408  cnph 8422  ipasslem2 8435  ipasslem5 8438  ipdi 8447  ipsubdi 8453  ipblnfi 8460  ajmoi 8463  ubthlem3 8475  ubthlem5 8477  ubthlem6 8478  ubthlem7 8479  ubthlem10 8482  ubthlem11 8483  minveclem24 8512  minveclem25 8513  minveclem28 8516  htthlem8 8570  htthlem9 8571  sinper 8628  cosper 8629  efifolem7 8662  efif1lem5 8668  circgrpOLD 8677  efper 8686  axgroth3 8718  hvsubopr 8824  hvsubclt 8826  hvaddsubvalt 8841  hvpncant 8847  hvaddeq0t 8875  hvmulcant 8878  his5t 8892  his7t 8895  his2sub2t 8898  hlimcaui 9045  hhssnv 9073  shorth 9107  occllem6 9117  projlem25 9149  projlem26 9150  pjvalt 9177  pjeq2t 9179  chsscon2t 9363  chpsscon2t 9366  chdmm3t 9388  chdmm4t 9389  chdmj3t 9392  chdmj4t 9393  chj4t 9396  spansnmul 9426  cmcm2t 9499  fh1t 9501  fh2t 9502  cm2jt 9503  spansnsclt 9533  spansncv 9537  5oalem4 9542  homulclt 9625  homco1t 9667  homulasst 9668  hoadddit 9669  hosubnegt 9673  honegsubdit 9676  hosubsub2t 9678  hosub4t 9679  adjmo 9698  adjsymt 9699  cnvadj 9756  nmopub2tALT 9773  unoplint 9783  counopt 9784  nmfnleub2t 9789  hmoplint 9805  braaddt 9808  bramult 9809  kbmult 9818  lnopmult 9830  lnopaddmul 9836  lnopsubmul 9838  homco2t 9840  nmlnop0ALT 9858  lnopm 9863  lnophs 9864  lnopeq0 9870  unopbdt 9878  hmopdt 9885  nmophm 9899  lnopcon 9901  lnfnmul 9911  lnfnaddmul 9912  lnfncon 9928  nlelsh 9931  riesz3 9933  cnlnadjlem6 9943  adjlnopt 9957  adjmult 9963  adjco 9971  cnvbramult 9986  leopnmidt 10009  hmopidmpj 10018  pjadjco 10027  pjss1co 10029  pjnormss 10034  pjclem4 10065  pjadj2co 10070  pj3s 10073  pj3 10074  hstnmoct 10088  hstle1t 10091  hst1ht 10092  hstlet 10095  hstoht 10097  spansncv2t 10158  dmdmdt 10165  mdslmd1lem2 10190  mdslmd2 10194  atcveq0 10212  chcv1t 10219  chcv2t 10220  cvexchlem 10232  cvp 10239  atcv1t 10244  atexcht 10245  atoml 10246  atcvatlem 10249  irredlem2 10255  irred 10258  atdmd 10262  atmd2 10264  mdsymlem3 10269  mdsymlem5 10271  sumdmdlem 10281  sumdmdlem2 10282  cdj1 10294  cdj3lem1 10295  cdj3lem2b 10298  cdj3 10302  symggrpi 10340  cayleylem2 10344  11st22nd 10390  cnfilca 10487  iint 10514

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