Theorem sylan2 284

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan2b  285  sylan2br  286  syl2an  287  sylanr1  402  sylanr2  403  mpanr2  435  adantrl  470  adantrr  471  ancom2s  556  3adantr1  1141  3adantr2  1142  3adantr3  1143  syl3anr1  1269  syl3anr3  1271  dfbi3dc  1376  xordidc  1378  elabgt  2829  sbciegft  2943  csbtt  3019  csbnestgf  3057  copsex2t  4175  pofun  4242  onsucmin  4431  onsucelsucr  4432  onsucsssucr  4433  ordsucunielexmid  4454  ordsuc  4486  nlimsucg  4489  elnn  4527  xpsspw  4659  elxp4  5034  elxp5  5035  funimass2  5209  imain  5213  funimaexg  5215  f1ff1  5344  dff1o2  5380  resdif  5397  funbrfv  5468  fvelimab  5485  eqfnfv2  5527  fvimacnvi  5542  ffvresb  5591  fnressn  5614  fmptapd  5619  fnex  5650  rexima  5664  ralima  5665  f1elima  5682  fnotovb  5822  mpoeq12  5839  fovrn  5921  fnovrn  5926  ofrfval  5998  ofvalg  5999  cofunexg  6017  cofunex2g  6018  mpoexxg  6116  mpoexg  6117  f1o2ndf1  6133  spc2ed  6138  smodm2  6200  tfrlem9  6224  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  tfri3  6272  rdgtfr  6279  rdgruledefgg  6280  oav2  6367  oasuc  6368  omv2  6369  onasuc  6370  omsuc  6376  onmsuc  6377  nnaass  6389  nndi  6390  nndir  6394  nnaword  6415  ecelqsg  6490  iinerm  6509  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  fvdiagfn  6595  ixpssmap2g  6629  domentr  6693  xpdom1g  6735  fopwdom  6738  ssenen  6753  phplem3  6756  phplem4  6757  php5dom  6765  ssfilem  6777  diffitest  6789  ctssdccl  7004  pm54.43  7063  addclpi  7159  addasspig  7162  mulasspig  7164  distrpig  7165  mulcanpig  7167  nnppipi  7175  enqdc1  7194  addassnqg  7214  ltbtwnnqq  7247  prarloclemarch  7250  prarloclemarch2  7251  enq0sym  7264  enq0ref  7265  addclnq0  7283  nqpnq0nq  7285  nnanq0  7290  distrnq0  7291  addassnq0lemcl  7293  addassnq0  7294  distnq0r  7295  prarloclemlt  7325  genpassl  7356  genpassu  7357  genpassg  7358  nqpru  7384  addcomprg  7410  mulcomprg  7412  distrlem1prl  7414  distrlem1pru  7415  1idprl  7422  1idpru  7423  recexprlemdisj  7462  recexprlem1ssl  7465  peano2nnnn  7685  ax1rid  7709  axcaucvglemcl  7727  le2tri3i  7896  add4  7947  cnegexlem1  7961  cnegexlem3  7963  cnegex  7964  subadd  7989  addsub  7997  addsubeq4  8001  negdi  8043  renegcl  8047  resubcl  8050  subdi  8171  mulneg2  8182  mul2neg  8184  submul2  8185  ltnegcon2  8250  lenegcon2  8253  lesub0  8265  cru  8388  recextlem1  8436  recexap  8438  div12ap  8478  divnegap  8490  letrp1  8630  dfinfre  8738  peano2nn  8756  nndivre  8780  nnsub  8783  nndivtr  8786  arch  8998  bndndx  9000  nn0addge1  9047  nn0addge2  9048  zaddcl  9118  zsubcl  9119  zltnle  9124  zrevaddcl  9128  nzadd  9130  zleltp1  9133  zltlem1  9135  zdiv  9163  peano2uz2  9182  uzind  9186  eluzp1l  9374  ublbneg  9432  qaddcl  9454  qsubcl  9457  qreccl  9461  qdivcl  9462  qrevaddcl  9463  irradd  9465  irrmul  9466  rerpdivcl  9501  nn0ledivnn  9584  xrre  9633  rexsub  9666  xaddass  9682  xnpcan  9685  xsubge0  9694  xposdif  9695  elioc2  9749  icoshft  9803  iccdil  9811  fzss2  9875  fzsuc2  9890  fzrev2  9896  elfzm11  9902  elfzp1b  9908  fzrevral  9916  fzshftral  9919  fzof  9952  fzoval  9956  fzon  9974  fzosubel  10002  zpnn0elfzo  10015  elfzom1b  10037  qltnle  10054  flqlt  10087  flqbi  10094  flqaddz  10101  fzofig  10236  seq3feq2  10274  ser3le  10322  expp1  10331  expm1t  10352  expeq0  10355  binom2sub  10436  bernneq  10443  expnlbnd  10447  faccl  10513  facdiv  10516  bcpasc  10544  bccl  10545  ffz0hash  10608  fnfzo0hash  10610  2shfti  10635  crim  10662  mulreap  10668  resub  10674  imsub  10682  ipcnval  10690  cjsub  10696  resqrexlemfp1  10813  resqrexlemgt0  10824  sqabsadd  10859  sqabssub  10860  abs2dif2  10911  cau3lem  10918  icodiamlt  10984  xrmaxaddlem  11061  clim  11082  clim2  11084  clim2c  11085  clim0c  11087  2clim  11102  climabs0  11108  climcn1  11109  climcn2  11110  climsqz  11136  climsqz2  11137  climub  11145  climserle  11146  fsum3cvg  11179  fisumss  11193  fsum3ser  11198  sumsplitdc  11233  fsump1i  11234  fsumlessfi  11261  telfsumo  11267  fsumparts  11271  iserabs  11276  binomlem  11284  isumsplit  11292  isum1p  11293  isumlessdc  11297  mertenslem2  11337  mertensabs  11338  prodfap0  11346  prodfrecap  11347  prodfdivap  11348  fproddccvg  11373  prodmodclem2  11378  ege2le3  11414  efsub  11424  efexp  11425  efsep  11434  sinsub  11483  cossub  11484  demoivre  11515  eirraplem  11519  moddvds  11538  0dvds  11549  iddvdsexp  11553  dvdssub  11574  dvdsle  11578  dvdsleabs  11579  dvdseq  11582  dvdsflip  11585  mulsucdiv2z  11618  divalgb  11658  divalg2  11659  ndvdsadd  11664  gcdneg  11706  gcdabs2  11714  modgcd  11715  bezoutlemsup  11733  gcdmultiplez  11745  gcdeq  11747  dvdssq  11755  lcmcllem  11784  lcmneg  11791  lcmdvds  11796  qredeu  11814  cncongrcoprm  11823  isprm3  11835  prmrp  11859  divnumden  11910  phiprmpw  11934  crth  11936  hashgcdlem  11939  hashgcdeq  11940  setsresg  12036  iunopn  12208  unopn  12211  eltg  12260  eltg2  12261  tgcl  12272  tgiun  12281  tgidm  12282  isopn3i  12343  isneip  12354  neipsm  12362  restbasg  12376  restopn2  12391  lmbrf  12423  cnclima  12431  lmss  12454  txbasval  12475  txlm  12487  psmetxrge0  12540  blininf  12632  blssps  12635  blss  12636  elmopn2  12657  bdmet  12710  metrest  12714  bl2ioo  12750  dvcjbr  12880  efper  12936  sinperlem  12937  abssinper  12975  cxpexprp  13024  logcxp  13026  rpcxpcl  13032  rpcxproot  13042  rprelogbmulexp  13081  bj-inex  13276  peano5set  13309  findset  13314  bj-findis  13348  nninfsellemsuc  13383  nninfself  13384  cvgcmp2nlemabs  13402  trilpolemeq1  13408  iooref1o  13426