Theorem sylan2 280

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan2.1	⊢ (𝜑 → 𝜒)
sylan2.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 271	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 276	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  sylan2b  281  sylan2br  282  syl2an  283  sylanr1  396  sylanr2  397  mpanr2  429  adantrl  462  adantrr  463  ancom2s  531  3adantr1  1100  3adantr2  1101  3adantr3  1102  syl3anr1  1224  syl3anr3  1226  dfbi3dc  1331  xordidc  1333  elabgt  2748  sbciegft  2858  csbtt  2932  csbnestgf  2969  copsex2t  4048  pofun  4115  onsucmin  4299  onsucelsucr  4300  onsucsssucr  4301  ordsucunielexmid  4322  ordsuc  4354  nlimsucg  4357  elnn  4395  xpsspw  4520  elxp4  4886  elxp5  4887  funimass2  5059  imain  5063  funimaexg  5065  f1ff1  5189  dff1o2  5223  resdif  5240  funbrfv  5308  fvelimab  5325  eqfnfv2  5363  fvimacnvi  5378  ffvresb  5426  fnressn  5448  fmptapd  5453  fnex  5482  rexima  5497  ralima  5498  f1elima  5515  fnotovb  5651  mpt2eq12  5668  fovrn  5746  fnovrn  5751  ofrfval  5823  fnofval  5824  cofunexg  5841  cofunex2g  5842  mpt2exxg  5936  mpt2exg  5937  f1o2ndf1  5952  spc2ed  5957  smodm2  6016  tfrlem9  6040  tfrlemibxssdm  6048  tfr1onlembxssdm  6064  tfrcllembxssdm  6077  tfri3  6088  rdgtfr  6095  rdgruledefgg  6096  oav2  6180  oasuc  6181  omv2  6182  onasuc  6183  omsuc  6189  onmsuc  6190  nnaass  6202  nndi  6203  nndir  6207  nnaword  6224  ecelqsg  6299  iinerm  6318  ecovass  6355  ecoviass  6356  ecovdi  6357  ecovidi  6358  fvdiagfn  6404  domentr  6462  xpdom1g  6503  fopwdom  6506  ssenen  6521  phplem3  6524  phplem4  6525  php5dom  6533  ssfilem  6545  diffitest  6557  pm54.43  6765  addclpi  6833  addasspig  6836  mulasspig  6838  distrpig  6839  mulcanpig  6841  nnppipi  6849  enqdc1  6868  addassnqg  6888  ltbtwnnqq  6921  prarloclemarch  6924  prarloclemarch2  6925  enq0sym  6938  enq0ref  6939  addclnq0  6957  nqpnq0nq  6959  nnanq0  6964  distrnq0  6965  addassnq0lemcl  6967  addassnq0  6968  distnq0r  6969  prarloclemlt  6999  genpassl  7030  genpassu  7031  genpassg  7032  nqpru  7058  addcomprg  7084  mulcomprg  7086  distrlem1prl  7088  distrlem1pru  7089  1idprl  7096  1idpru  7097  recexprlemdisj  7136  recexprlem1ssl  7139  peano2nnnn  7337  ax1rid  7359  axcaucvglemcl  7377  le2tri3i  7540  add4  7590  cnegexlem1  7604  cnegexlem3  7606  cnegex  7607  subadd  7632  addsub  7640  addsubeq4  7644  negdi  7686  renegcl  7690  resubcl  7693  subdi  7810  mulneg2  7821  mul2neg  7823  submul2  7824  ltnegcon2  7889  lenegcon2  7892  lesub0  7904  cru  8023  recextlem1  8062  recexap  8064  div12ap  8103  divnegap  8115  letrp1  8247  dfinfre  8355  peano2nn  8372  nndivre  8395  nnsub  8398  nndivtr  8401  arch  8606  bndndx  8608  nn0addge1  8655  nn0addge2  8656  zaddcl  8726  zsubcl  8727  zltnle  8732  zrevaddcl  8736  nzadd  8738  zleltp1  8741  zltlem1  8743  zdiv  8770  peano2uz2  8789  uzind  8793  eluzp1l  8978  ublbneg  9033  qaddcl  9055  qsubcl  9058  qreccl  9062  qdivcl  9063  qrevaddcl  9064  irradd  9066  irrmul  9067  rerpdivcl  9099  nn0ledivnn  9173  xrre  9217  elioc2  9289  icoshft  9342  iccdil  9350  fzss2  9412  fzsuc2  9426  fzrev2  9432  elfzm11  9438  elfzp1b  9444  fzrevral  9452  fzshftral  9455  fzof  9486  fzoval  9490  fzon  9508  fzosubel  9536  zpnn0elfzo  9549  elfzom1b  9571  qltnle  9588  flqlt  9621  flqbi  9628  flqaddz  9635  fzofig  9770  iseqfeq2  9821  iseqfeq  9823  iseqsplit  9832  ser3le  9873  expp1  9882  expm1t  9903  expeq0  9906  binom2sub  9986  bernneq  9992  expnlbnd  9996  faccl  10061  facdiv  10064  bcpasc  10092  bccl  10093  ffz0hash  10156  fnfzo0hash  10158  2shfti  10183  crim  10209  mulreap  10215  resub  10221  imsub  10229  ipcnval  10237  cjsub  10243  resqrexlemfp1  10359  resqrexlemgt0  10370  sqabsadd  10405  sqabssub  10406  abs2dif2  10457  cau3lem  10464  icodiamlt  10530  clim  10585  clim2  10587  clim2c  10588  clim0c  10590  2clim  10605  climabs0  10612  climcn1  10613  climcn2  10614  climsqz  10639  climsqz2  10640  climub  10648  climserile  10649  fisumcvg  10680  fisumss  10694  moddvds  10730  0dvds  10741  iddvdsexp  10745  dvdssub  10766  dvdsle  10770  dvdsleabs  10771  dvdseq  10774  dvdsflip  10777  mulsucdiv2z  10810  divalgb  10850  divalg2  10851  ndvdsadd  10856  gcdneg  10898  gcdabs2  10906  modgcd  10907  bezoutlemsup  10923  gcdmultiplez  10935  gcdeq  10937  dvdssq  10945  lcmcllem  10974  lcmneg  10981  lcmdvds  10986  qredeu  11004  cncongrcoprm  11013  isprm3  11025  prmrp  11049  divnumden  11099  phiprmpw  11123  crth  11125  hashgcdlem  11128  hashgcdeq  11129  bj-inex  11286  peano5set  11323  findset  11328  bj-findis  11362  nninfsellemsuc  11392  nninfself  11393