Theorem sylan2 281

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 272	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 277	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan2b  282  sylan2br  283  syl2an  284  sylanr1  397  sylanr2  398  mpanr2  430  adantrl  463  adantrr  464  ancom2s  534  3adantr1  1105  3adantr2  1106  3adantr3  1107  syl3anr1  1233  syl3anr3  1235  dfbi3dc  1340  xordidc  1342  elabgt  2771  sbciegft  2883  csbtt  2957  csbnestgf  2994  copsex2t  4096  pofun  4163  onsucmin  4352  onsucelsucr  4353  onsucsssucr  4354  ordsucunielexmid  4375  ordsuc  4407  nlimsucg  4410  elnn  4448  xpsspw  4579  elxp4  4952  elxp5  4953  funimass2  5126  imain  5130  funimaexg  5132  f1ff1  5259  dff1o2  5293  resdif  5310  funbrfv  5378  fvelimab  5395  eqfnfv2  5437  fvimacnvi  5452  ffvresb  5500  fnressn  5522  fmptapd  5527  fnex  5558  rexima  5572  ralima  5573  f1elima  5590  fnotovb  5730  mpt2eq12  5747  fovrn  5825  fnovrn  5830  ofrfval  5902  fnofval  5903  cofunexg  5920  cofunex2g  5921  mpt2exxg  6015  mpt2exg  6016  f1o2ndf1  6031  spc2ed  6036  smodm2  6098  tfrlem9  6122  tfrlemibxssdm  6130  tfr1onlembxssdm  6146  tfrcllembxssdm  6159  tfri3  6170  rdgtfr  6177  rdgruledefgg  6178  oav2  6264  oasuc  6265  omv2  6266  onasuc  6267  omsuc  6273  onmsuc  6274  nnaass  6286  nndi  6287  nndir  6291  nnaword  6310  ecelqsg  6385  iinerm  6404  ecovass  6441  ecoviass  6442  ecovdi  6443  ecovidi  6444  fvdiagfn  6490  ixpssmap2g  6524  domentr  6588  xpdom1g  6629  fopwdom  6632  ssenen  6647  phplem3  6650  phplem4  6651  php5dom  6659  ssfilem  6671  diffitest  6683  pm54.43  6915  addclpi  6983  addasspig  6986  mulasspig  6988  distrpig  6989  mulcanpig  6991  nnppipi  6999  enqdc1  7018  addassnqg  7038  ltbtwnnqq  7071  prarloclemarch  7074  prarloclemarch2  7075  enq0sym  7088  enq0ref  7089  addclnq0  7107  nqpnq0nq  7109  nnanq0  7114  distrnq0  7115  addassnq0lemcl  7117  addassnq0  7118  distnq0r  7119  prarloclemlt  7149  genpassl  7180  genpassu  7181  genpassg  7182  nqpru  7208  addcomprg  7234  mulcomprg  7236  distrlem1prl  7238  distrlem1pru  7239  1idprl  7246  1idpru  7247  recexprlemdisj  7286  recexprlem1ssl  7289  peano2nnnn  7487  ax1rid  7509  axcaucvglemcl  7527  le2tri3i  7690  add4  7740  cnegexlem1  7754  cnegexlem3  7756  cnegex  7757  subadd  7782  addsub  7790  addsubeq4  7794  negdi  7836  renegcl  7840  resubcl  7843  subdi  7960  mulneg2  7971  mul2neg  7973  submul2  7974  ltnegcon2  8039  lenegcon2  8042  lesub0  8054  cru  8176  recextlem1  8217  recexap  8219  div12ap  8258  divnegap  8270  letrp1  8406  dfinfre  8514  peano2nn  8532  nndivre  8556  nnsub  8559  nndivtr  8562  arch  8768  bndndx  8770  nn0addge1  8817  nn0addge2  8818  zaddcl  8888  zsubcl  8889  zltnle  8894  zrevaddcl  8898  nzadd  8900  zleltp1  8903  zltlem1  8905  zdiv  8933  peano2uz2  8952  uzind  8956  eluzp1l  9142  ublbneg  9197  qaddcl  9219  qsubcl  9222  qreccl  9226  qdivcl  9227  qrevaddcl  9228  irradd  9230  irrmul  9231  rerpdivcl  9263  nn0ledivnn  9337  xrre  9386  rexsub  9419  xaddass  9435  xnpcan  9438  xsubge0  9447  xposdif  9448  elioc2  9502  icoshft  9556  iccdil  9564  fzss2  9627  fzsuc2  9642  fzrev2  9648  elfzm11  9654  elfzp1b  9660  fzrevral  9668  fzshftral  9671  fzof  9704  fzoval  9708  fzon  9726  fzosubel  9754  zpnn0elfzo  9767  elfzom1b  9789  qltnle  9806  flqlt  9839  flqbi  9846  flqaddz  9853  fzofig  9988  seq3feq2  10020  ser3le  10068  expp1  10077  expm1t  10098  expeq0  10101  binom2sub  10182  bernneq  10189  expnlbnd  10193  faccl  10258  facdiv  10261  bcpasc  10289  bccl  10290  ffz0hash  10353  fnfzo0hash  10355  2shfti  10380  crim  10407  mulreap  10413  resub  10419  imsub  10427  ipcnval  10435  cjsub  10441  resqrexlemfp1  10557  resqrexlemgt0  10568  sqabsadd  10603  sqabssub  10604  abs2dif2  10655  cau3lem  10662  icodiamlt  10728  xrmaxaddlem  10803  clim  10824  clim2  10826  clim2c  10827  clim0c  10829  2clim  10844  climabs0  10850  climcn1  10851  climcn2  10852  climsqz  10878  climsqz2  10879  climub  10887  climserle  10888  fsum3cvg  10920  fisumss  10935  fsum3ser  10940  sumsplitdc  10975  fsump1i  10976  fsumlessfi  11003  telfsumo  11009  fsumparts  11013  iserabs  11018  binomlem  11026  isumsplit  11034  isum1p  11035  isumlessdc  11039  mertenslem2  11079  mertensabs  11080  ege2le3  11110  efsub  11120  efexp  11121  efsep  11130  sinsub  11180  cossub  11181  demoivre  11211  eirraplem  11213  moddvds  11232  0dvds  11243  iddvdsexp  11247  dvdssub  11268  dvdsle  11272  dvdsleabs  11273  dvdseq  11276  dvdsflip  11279  mulsucdiv2z  11312  divalgb  11352  divalg2  11353  ndvdsadd  11358  gcdneg  11400  gcdabs2  11408  modgcd  11409  bezoutlemsup  11425  gcdmultiplez  11437  gcdeq  11439  dvdssq  11447  lcmcllem  11476  lcmneg  11483  lcmdvds  11488  qredeu  11506  cncongrcoprm  11515  isprm3  11527  prmrp  11551  divnumden  11601  phiprmpw  11625  crth  11627  hashgcdlem  11630  hashgcdeq  11631  setsresg  11681  iunopn  11853  unopn  11856  eltg  11904  eltg2  11905  tgcl  11916  tgiun  11925  tgidm  11926  isopn3i  11987  isneip  11998  neipsm  12006  restbasg  12020  restopn2  12035  lmbrf  12066  cnclima  12074  lmss  12097  psmetxrge0  12118  blininf  12210  blssps  12213  blss  12214  elmopn2  12235  bdmet  12288  metrest  12292  bl2ioo  12318  bj-inex  12515  peano5set  12552  findset  12557  bj-findis  12591  nninfsellemsuc  12618  nninfself  12619