Theorem sylan2 286

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  404  sylanr2  405  mpanr2  438  adantrl  478  adantrr  479  ancom2s  566  annimdc  939  3adantr1  1158  3adantr2  1159  3adantr3  1160  syl3anr1  1301  syl3anr3  1303  dfbi3dc  1408  xordidc  1410  elabgt  2905  sbciegft  3020  csbtt  3096  csbnestgf  3137  copsex2t  4279  pofun  4348  onsucmin  4544  onsucelsucr  4545  onsucsssucr  4546  ordsucunielexmid  4568  ordsuc  4600  nlimsucg  4603  elnn  4643  xpsspw  4776  elxp4  5158  elxp5  5159  funimass2  5337  imain  5341  funimaexg  5343  f1ff1  5474  dff1o2  5512  resdif  5529  funbrfv  5602  fvelimab  5620  eqfnfv2  5663  fvimacnvi  5679  ffvresb  5728  fnressn  5751  fmptapd  5756  fnex  5787  rexima  5804  ralima  5805  f1elima  5823  fnotovb  5969  mpoeq12  5986  fovcdm  6070  fnovrn  6075  ofrfval  6148  ofvalg  6149  cofunexg  6175  cofunex2g  6176  mpoexxg  6277  mpoexg  6278  f1o2ndf1  6295  spc2ed  6300  smodm2  6362  tfrlem9  6386  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  tfri3  6434  rdgtfr  6441  rdgruledefgg  6442  oav2  6530  oasuc  6531  omv2  6532  onasuc  6533  omsuc  6539  onmsuc  6540  nnaass  6552  nndi  6553  nndir  6557  nnaword  6578  ecelqsg  6656  iinerm  6675  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  fvdiagfn  6761  ixpssmap2g  6795  domentr  6859  xpdom1g  6901  fopwdom  6906  ssenen  6921  phplem3  6924  phplem4  6925  php5dom  6933  ssfilem  6945  diffitest  6957  ctssdccl  7186  pm54.43  7271  addclpi  7413  addasspig  7416  mulasspig  7418  distrpig  7419  mulcanpig  7421  nnppipi  7429  enqdc1  7448  addassnqg  7468  ltbtwnnqq  7501  prarloclemarch  7504  prarloclemarch2  7505  enq0sym  7518  enq0ref  7519  addclnq0  7537  nqpnq0nq  7539  nnanq0  7544  distrnq0  7545  addassnq0lemcl  7547  addassnq0  7548  distnq0r  7549  prarloclemlt  7579  genpassl  7610  genpassu  7611  genpassg  7612  nqpru  7638  addcomprg  7664  mulcomprg  7666  distrlem1prl  7668  distrlem1pru  7669  1idprl  7676  1idpru  7677  recexprlemdisj  7716  recexprlem1ssl  7719  peano2nnnn  7939  ax1rid  7963  axcaucvglemcl  7981  le2tri3i  8154  add4  8206  cnegexlem1  8220  cnegexlem3  8222  cnegex  8223  subadd  8248  addsub  8256  addsubeq4  8260  negdi  8302  renegcl  8306  resubcl  8309  subdi  8430  mulneg2  8441  mul2neg  8443  submul2  8444  ltnegcon2  8510  lenegcon2  8513  lesub0  8525  cru  8648  recextlem1  8697  recexap  8699  div12ap  8740  divnegap  8752  letrp1  8894  dfinfre  9002  peano2nn  9021  nndivre  9045  nnsub  9048  nndivtr  9051  arch  9265  bndndx  9267  nn0addge1  9314  nn0addge2  9315  zaddcl  9385  zsubcl  9386  zltnle  9391  zrevaddcl  9395  nzadd  9397  zleltp1  9400  zltlem1  9402  zdiv  9433  peano2uz2  9452  uzind  9456  eluzp1l  9645  ublbneg  9706  qaddcl  9728  qsubcl  9731  qreccl  9735  qdivcl  9736  qrevaddcl  9737  irradd  9739  irrmul  9740  rerpdivcl  9778  nn0ledivnn  9861  xrre  9914  rexsub  9947  xaddass  9963  xnpcan  9966  xsubge0  9975  xposdif  9976  elioc2  10030  icoshft  10084  iccdil  10092  fzss2  10158  fzsuc2  10173  fzrev2  10179  elfzm11  10185  elfzp1b  10191  fzrevral  10199  fzshftral  10202  fzof  10238  fzoval  10242  fzon  10261  fzosubel  10289  zpnn0elfzo  10302  elfzom1b  10324  qltnle  10352  flqlt  10392  flqbi  10399  flqaddz  10406  fzofig  10543  seq3feq2  10587  ser3le  10648  expp1  10657  expm1t  10678  expeq0  10681  binom2sub  10764  bernneq  10771  expnlbnd  10775  zzlesq  10819  faccl  10846  facdiv  10849  bcpasc  10877  bccl  10878  ffz0hash  10944  fnfzo0hash  10946  wrdlen1  10991  wrdred1  10996  2shfti  11015  crim  11042  mulreap  11048  resub  11054  imsub  11062  ipcnval  11070  cjsub  11076  resqrexlemfp1  11193  resqrexlemgt0  11204  sqabsadd  11239  sqabssub  11240  abs2dif2  11291  cau3lem  11298  icodiamlt  11364  xrmaxaddlem  11444  clim  11465  clim2  11467  clim2c  11468  clim0c  11470  2clim  11485  climabs0  11491  climcn1  11492  climcn2  11493  climsqz  11519  climsqz2  11520  climub  11528  climserle  11529  fsum3cvg  11562  fisumss  11576  fsum3ser  11581  sumsplitdc  11616  fsump1i  11617  fsumlessfi  11644  telfsumo  11650  fsumparts  11654  iserabs  11659  binomlem  11667  isumsplit  11675  isum1p  11676  isumlessdc  11680  mertenslem2  11720  mertensabs  11721  prodfap0  11729  prodfrecap  11730  prodfdivap  11731  fproddccvg  11756  prodmodclem2  11761  fprodssdc  11774  fprodabs  11800  fprodeq0  11801  fprodeq0g  11822  ege2le3  11855  efsub  11865  efexp  11866  efsep  11875  sinsub  11924  cossub  11925  demoivre  11957  eirraplem  11961  moddvds  11983  0dvds  11995  iddvdsexp  11999  dvdssub  12022  dvdsle  12028  dvdsleabs  12029  dvdseq  12032  dvdsflip  12035  mulsucdiv2z  12069  divalgb  12109  divalg2  12110  ndvdsadd  12115  bitsp1  12135  gcdneg  12176  gcdabs2  12184  modgcd  12185  bezoutlemsup  12203  gcdmultiplez  12215  gcdeq  12217  dvdssq  12225  lcmcllem  12262  lcmneg  12269  lcmdvds  12274  qredeu  12292  cncongrcoprm  12301  isprm3  12313  prmrp  12340  divnumden  12391  phiprmpw  12417  crth  12419  hashgcdlem  12433  hashgcdeq  12435  modprminv  12445  modprminveq  12446  modprmn0modprm0  12452  coprimeprodsq2  12454  pcpre1  12488  pccl  12495  pcmul  12497  pcdiv  12498  pcqcl  12502  pcexp  12505  pcdvds  12511  pcndvds  12513  pcndvds2  12515  pcelnn  12517  pcgcd1  12524  pc2dvds  12526  pc11  12527  gzsubcl  12576  4sqlem3  12586  setsresg  12743  pwssnf1o  13002  xpsfeq  13049  submcl  13183  grpinvnzcl  13276  mulgnnass  13365  nmzsubg  13418  nmznsg  13421  resghm2b  13470  ghmnsgpreima  13477  gsumfzsnfd  13553  iscrng2  13649  subrngpropd  13850  issubrg3  13881  subrgpropd  13887  islmodd  13927  lss1d  14017  lspsncl  14026  lspsnid  14041  df2idl2  14143  2idlcpbl  14158  qusrhm  14162  gsumfzfsumlemm  14221  iunopn  14346  unopn  14349  eltg  14396  eltg2  14397  tgcl  14408  tgiun  14417  tgidm  14418  isopn3i  14479  isneip  14490  neipsm  14498  restbasg  14512  restopn2  14527  lmbrf  14559  cnclima  14567  lmss  14590  txbasval  14611  txlm  14623  psmetxrge0  14676  blininf  14768  blssps  14771  blss  14772  elmopn2  14793  bdmet  14846  metrest  14850  bl2ioo  14894  dvcjbr  15052  plyaddlem1  15091  plymullem1  15092  plyreres  15108  dvply1  15109  dvply2g  15110  efper  15151  sinperlem  15152  abssinper  15190  cxpexprp  15239  logcxp  15241  rpcxpcl  15247  rpcxproot  15258  rprelogbmulexp  15300  lgsval2lem  15359  lgssq2  15390  lgsprme0  15391  bj-inex  15661  peano5set  15694  findset  15699  bj-findis  15733  nninfsellemsuc  15767  nninfself  15768  cvgcmp2nlemabs  15789  iooref1o  15791  trilpolemeq1  15797  nconstwlpolemgt0  15821