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  568  annimdc  946  ifpnst  997  3adantr1  1183  3adantr2  1184  3adantr3  1185  syl3anr1  1326  syl3anr3  1328  dfbi3dc  1442  xordidc  1444  elabgt  2948  sbciegft  3063  csbtt  3140  csbnestgf  3181  copsex2t  4343  pofun  4415  onsucmin  4611  onsucelsucr  4612  onsucsssucr  4613  ordsucunielexmid  4635  ordsuc  4667  nlimsucg  4670  elnn  4710  xpsspw  4844  elxp4  5231  elxp5  5232  funimass2  5415  imain  5419  funimaexg  5421  f1ff1  5559  dff1o2  5597  resdif  5614  funbrfv  5691  fnbrfvb2  5697  fvelimab  5711  eqfnfv2  5754  fvimacnvi  5770  ffvresb  5818  fnressn  5848  fmptapd  5853  fnex  5884  rexima  5905  ralima  5906  f1elima  5924  fnotovb  6074  mpoeq12  6091  fovcdm  6175  fnovrn  6180  ofrfval  6253  ofvalg  6254  cofunexg  6280  cofunex2g  6281  mpoexxg  6384  mpoexg  6385  f1o2ndf1  6402  spc2ed  6407  funsssuppss  6436  smodm2  6504  tfrlem9  6528  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  tfri3  6576  rdgtfr  6583  rdgruledefgg  6584  oav2  6674  oasuc  6675  omv2  6676  onasuc  6677  omsuc  6683  onmsuc  6684  nnaass  6696  nndi  6697  nndir  6701  nnaword  6722  ecelqsg  6800  iinerm  6819  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  fvdiagfn  6905  ixpssmap2g  6939  domentr  7008  xpdom1g  7060  fopwdom  7065  ssenen  7080  phplem3  7083  phplem4  7084  php5dom  7092  ssfilem  7105  ssfilemd  7107  diffitest  7119  ctssdccl  7353  pm54.43  7438  pw1if  7486  addclpi  7590  addasspig  7593  mulasspig  7595  distrpig  7596  mulcanpig  7598  nnppipi  7606  enqdc1  7625  addassnqg  7645  ltbtwnnqq  7678  prarloclemarch  7681  prarloclemarch2  7682  enq0sym  7695  enq0ref  7696  addclnq0  7714  nqpnq0nq  7716  nnanq0  7721  distrnq0  7722  addassnq0lemcl  7724  addassnq0  7725  distnq0r  7726  prarloclemlt  7756  genpassl  7787  genpassu  7788  genpassg  7789  nqpru  7815  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  1idprl  7853  1idpru  7854  recexprlemdisj  7893  recexprlem1ssl  7896  peano2nnnn  8116  ax1rid  8140  axcaucvglemcl  8158  le2tri3i  8331  add4  8383  cnegexlem1  8397  cnegexlem3  8399  cnegex  8400  subadd  8425  addsub  8433  addsubeq4  8437  negdi  8479  renegcl  8483  resubcl  8486  subdi  8607  mulneg2  8618  mul2neg  8620  submul2  8621  ltnegcon2  8687  lenegcon2  8690  lesub0  8702  cru  8825  recextlem1  8874  recexap  8876  div12ap  8917  divnegap  8929  letrp1  9071  dfinfre  9179  peano2nn  9198  nndivre  9222  nnsub  9225  nndivtr  9228  arch  9442  bndndx  9444  nn0addge1  9491  nn0addge2  9492  zaddcl  9564  zsubcl  9565  zltnle  9570  zrevaddcl  9575  nzadd  9577  zleltp1  9580  zltlem1  9582  zdiv  9613  peano2uz2  9632  uzind  9636  eluzp1l  9826  ublbneg  9892  qaddcl  9914  qsubcl  9917  qreccl  9921  qdivcl  9922  qrevaddcl  9923  irradd  9925  irrmul  9926  rerpdivcl  9964  nn0ledivnn  10047  xrre  10100  rexsub  10133  xaddass  10149  xnpcan  10152  xsubge0  10161  xposdif  10162  elioc2  10216  icoshft  10270  iccdil  10278  fzss2  10344  fzsuc2  10359  fzrev2  10365  elfzm11  10371  elfzp1b  10377  fzrevral  10385  fzshftral  10388  fzof  10424  fzoval  10428  fzon  10447  elfzoextl  10482  fzosubel  10485  zpnn0elfzo  10498  elfzom1b  10520  qltnle  10549  flqlt  10589  flqbi  10596  flqaddz  10603  fzofig  10740  seq3feq2  10784  ser3le  10845  expp1  10854  expm1t  10875  expeq0  10878  binom2sub  10961  bernneq  10968  expnlbnd  10972  zzlesq  11016  faccl  11043  facdiv  11046  bcpasc  11074  bccl  11075  ffz0hash  11143  fnfzo0hash  11145  wrdlen1  11200  wrdred1  11205  ccatval21sw  11231  wrdl1exs1  11255  ccatws1cl  11258  ccatws1leng  11260  pfxmpt  11310  pfxfv  11314  pfxfvlsw  11325  ccatpfx  11331  pfx1  11333  swrdccatin1  11355  swrdccat  11365  pfxccatpfx1  11366  2shfti  11454  crim  11481  mulreap  11487  resub  11493  imsub  11501  ipcnval  11509  cjsub  11515  resqrexlemfp1  11632  resqrexlemgt0  11643  sqabsadd  11678  sqabssub  11679  abs2dif2  11730  cau3lem  11737  icodiamlt  11803  xrmaxaddlem  11883  clim  11904  clim2  11906  clim2c  11907  clim0c  11909  2clim  11924  climabs0  11930  climcn1  11931  climcn2  11932  climsqz  11958  climsqz2  11959  climub  11967  climserle  11968  fsum3cvg  12002  fisumss  12016  fsum3ser  12021  sumsplitdc  12056  fsump1i  12057  fsumlessfi  12084  telfsumo  12090  fsumparts  12094  iserabs  12099  binomlem  12107  isumsplit  12115  isum1p  12116  isumlessdc  12120  mertenslem2  12160  mertensabs  12161  prodfap0  12169  prodfrecap  12170  prodfdivap  12171  fproddccvg  12196  prodmodclem2  12201  fprodssdc  12214  fprodabs  12240  fprodeq0  12241  fprodeq0g  12262  ege2le3  12295  efsub  12305  efexp  12306  efsep  12315  sinsub  12364  cossub  12365  demoivre  12397  eirraplem  12401  moddvds  12423  0dvds  12435  iddvdsexp  12439  dvdssub  12462  dvdsle  12468  dvdsleabs  12469  dvdseq  12472  dvdsflip  12475  mulsucdiv2z  12509  divalgb  12549  divalg2  12550  ndvdsadd  12555  bitsp1  12575  gcdneg  12616  gcdabs2  12624  modgcd  12625  bezoutlemsup  12643  gcdmultiplez  12655  gcdeq  12657  dvdssq  12665  lcmcllem  12702  lcmneg  12709  lcmdvds  12714  qredeu  12732  cncongrcoprm  12741  isprm3  12753  prmrp  12780  divnumden  12831  phiprmpw  12857  crth  12859  hashgcdlem  12873  hashgcdeq  12875  modprminv  12885  modprminveq  12886  modprmn0modprm0  12892  coprimeprodsq2  12894  pcpre1  12928  pccl  12935  pcmul  12937  pcdiv  12938  pcqcl  12942  pcexp  12945  pcdvds  12951  pcndvds  12953  pcndvds2  12955  pcelnn  12957  pcgcd1  12964  pc2dvds  12966  pc11  12967  gzsubcl  13016  4sqlem3  13026  setsresg  13183  pwssnf1o  13444  xpsfeq  13491  submcl  13625  grpinvnzcl  13718  mulgnnass  13807  nmzsubg  13860  nmznsg  13863  resghm2b  13912  ghmnsgpreima  13919  gsumfzsnfd  13995  iscrng2  14092  subrngpropd  14294  issubrg3  14325  subrgpropd  14331  islmodd  14372  lss1d  14462  lspsncl  14471  lspsnid  14486  df2idl2  14588  2idlcpbl  14603  qusrhm  14607  gsumfzfsumlemm  14666  iunopn  14796  unopn  14799  eltg  14846  eltg2  14847  tgcl  14858  tgiun  14867  tgidm  14868  isopn3i  14929  isneip  14940  neipsm  14948  restbasg  14962  restopn2  14977  lmbrf  15009  cnclima  15017  lmss  15040  txbasval  15061  txlm  15073  psmetxrge0  15126  blininf  15218  blssps  15221  blss  15222  elmopn2  15243  bdmet  15296  metrest  15300  bl2ioo  15344  dvcjbr  15502  plyaddlem1  15541  plymullem1  15542  plyreres  15558  dvply1  15559  dvply2g  15560  efper  15601  sinperlem  15602  abssinper  15640  cxpexprp  15689  logcxp  15691  rpcxpcl  15697  rpcxproot  15708  rprelogbmulexp  15750  lgsval2lem  15812  lgssq2  15843  lgsprme0  15844  ausgrusgrben  16092  wlkepvtx  16299  bj-inex  16606  peano5set  16639  findset  16644  bj-findis  16678  nninfsellemsuc  16721  nninfself  16722  cvgcmp2nlemabs  16747  iooref1o  16749  trilpolemeq1  16755  nconstwlpolemgt0  16780