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  943  ifpnst  994  3adantr1  1180  3adantr2  1181  3adantr3  1182  syl3anr1  1323  syl3anr3  1325  dfbi3dc  1439  xordidc  1441  elabgt  2945  sbciegft  3060  csbtt  3137  csbnestgf  3178  copsex2t  4335  pofun  4407  onsucmin  4603  onsucelsucr  4604  onsucsssucr  4605  ordsucunielexmid  4627  ordsuc  4659  nlimsucg  4662  elnn  4702  xpsspw  4836  elxp4  5222  elxp5  5223  funimass2  5405  imain  5409  funimaexg  5411  f1ff1  5547  dff1o2  5585  resdif  5602  funbrfv  5678  fnbrfvb2  5684  fvelimab  5698  eqfnfv2  5741  fvimacnvi  5757  ffvresb  5806  fnressn  5835  fmptapd  5840  fnex  5871  rexima  5890  ralima  5891  f1elima  5909  fnotovb  6059  mpoeq12  6076  fovcdm  6160  fnovrn  6165  ofrfval  6239  ofvalg  6240  cofunexg  6266  cofunex2g  6267  mpoexxg  6370  mpoexg  6371  f1o2ndf1  6388  spc2ed  6393  smodm2  6456  tfrlem9  6480  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  tfri3  6528  rdgtfr  6535  rdgruledefgg  6536  oav2  6626  oasuc  6627  omv2  6628  onasuc  6629  omsuc  6635  onmsuc  6636  nnaass  6648  nndi  6649  nndir  6653  nnaword  6674  ecelqsg  6752  iinerm  6771  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  fvdiagfn  6857  ixpssmap2g  6891  domentr  6960  xpdom1g  7012  fopwdom  7017  ssenen  7032  phplem3  7035  phplem4  7036  php5dom  7044  ssfilem  7057  ssfilemd  7059  diffitest  7071  ctssdccl  7304  pm54.43  7389  pw1if  7436  addclpi  7540  addasspig  7543  mulasspig  7545  distrpig  7546  mulcanpig  7548  nnppipi  7556  enqdc1  7575  addassnqg  7595  ltbtwnnqq  7628  prarloclemarch  7631  prarloclemarch2  7632  enq0sym  7645  enq0ref  7646  addclnq0  7664  nqpnq0nq  7666  nnanq0  7671  distrnq0  7672  addassnq0lemcl  7674  addassnq0  7675  distnq0r  7676  prarloclemlt  7706  genpassl  7737  genpassu  7738  genpassg  7739  nqpru  7765  addcomprg  7791  mulcomprg  7793  distrlem1prl  7795  distrlem1pru  7796  1idprl  7803  1idpru  7804  recexprlemdisj  7843  recexprlem1ssl  7846  peano2nnnn  8066  ax1rid  8090  axcaucvglemcl  8108  le2tri3i  8281  add4  8333  cnegexlem1  8347  cnegexlem3  8349  cnegex  8350  subadd  8375  addsub  8383  addsubeq4  8387  negdi  8429  renegcl  8433  resubcl  8436  subdi  8557  mulneg2  8568  mul2neg  8570  submul2  8571  ltnegcon2  8637  lenegcon2  8640  lesub0  8652  cru  8775  recextlem1  8824  recexap  8826  div12ap  8867  divnegap  8879  letrp1  9021  dfinfre  9129  peano2nn  9148  nndivre  9172  nnsub  9175  nndivtr  9178  arch  9392  bndndx  9394  nn0addge1  9441  nn0addge2  9442  zaddcl  9512  zsubcl  9513  zltnle  9518  zrevaddcl  9523  nzadd  9525  zleltp1  9528  zltlem1  9530  zdiv  9561  peano2uz2  9580  uzind  9584  eluzp1l  9774  ublbneg  9840  qaddcl  9862  qsubcl  9865  qreccl  9869  qdivcl  9870  qrevaddcl  9871  irradd  9873  irrmul  9874  rerpdivcl  9912  nn0ledivnn  9995  xrre  10048  rexsub  10081  xaddass  10097  xnpcan  10100  xsubge0  10109  xposdif  10110  elioc2  10164  icoshft  10218  iccdil  10226  fzss2  10292  fzsuc2  10307  fzrev2  10313  elfzm11  10319  elfzp1b  10325  fzrevral  10333  fzshftral  10336  fzof  10372  fzoval  10376  fzon  10395  elfzoextl  10429  fzosubel  10432  zpnn0elfzo  10445  elfzom1b  10467  qltnle  10496  flqlt  10536  flqbi  10543  flqaddz  10550  fzofig  10687  seq3feq2  10731  ser3le  10792  expp1  10801  expm1t  10822  expeq0  10825  binom2sub  10908  bernneq  10915  expnlbnd  10919  zzlesq  10963  faccl  10990  facdiv  10993  bcpasc  11021  bccl  11022  ffz0hash  11090  fnfzo0hash  11092  wrdlen1  11144  wrdred1  11149  ccatval21sw  11175  wrdl1exs1  11199  ccatws1cl  11202  ccatws1leng  11204  pfxmpt  11254  pfxfv  11258  pfxfvlsw  11269  ccatpfx  11275  pfx1  11277  swrdccatin1  11299  swrdccat  11309  pfxccatpfx1  11310  2shfti  11385  crim  11412  mulreap  11418  resub  11424  imsub  11432  ipcnval  11440  cjsub  11446  resqrexlemfp1  11563  resqrexlemgt0  11574  sqabsadd  11609  sqabssub  11610  abs2dif2  11661  cau3lem  11668  icodiamlt  11734  xrmaxaddlem  11814  clim  11835  clim2  11837  clim2c  11838  clim0c  11840  2clim  11855  climabs0  11861  climcn1  11862  climcn2  11863  climsqz  11889  climsqz2  11890  climub  11898  climserle  11899  fsum3cvg  11932  fisumss  11946  fsum3ser  11951  sumsplitdc  11986  fsump1i  11987  fsumlessfi  12014  telfsumo  12020  fsumparts  12024  iserabs  12029  binomlem  12037  isumsplit  12045  isum1p  12046  isumlessdc  12050  mertenslem2  12090  mertensabs  12091  prodfap0  12099  prodfrecap  12100  prodfdivap  12101  fproddccvg  12126  prodmodclem2  12131  fprodssdc  12144  fprodabs  12170  fprodeq0  12171  fprodeq0g  12192  ege2le3  12225  efsub  12235  efexp  12236  efsep  12245  sinsub  12294  cossub  12295  demoivre  12327  eirraplem  12331  moddvds  12353  0dvds  12365  iddvdsexp  12369  dvdssub  12392  dvdsle  12398  dvdsleabs  12399  dvdseq  12402  dvdsflip  12405  mulsucdiv2z  12439  divalgb  12479  divalg2  12480  ndvdsadd  12485  bitsp1  12505  gcdneg  12546  gcdabs2  12554  modgcd  12555  bezoutlemsup  12573  gcdmultiplez  12585  gcdeq  12587  dvdssq  12595  lcmcllem  12632  lcmneg  12639  lcmdvds  12644  qredeu  12662  cncongrcoprm  12671  isprm3  12683  prmrp  12710  divnumden  12761  phiprmpw  12787  crth  12789  hashgcdlem  12803  hashgcdeq  12805  modprminv  12815  modprminveq  12816  modprmn0modprm0  12822  coprimeprodsq2  12824  pcpre1  12858  pccl  12865  pcmul  12867  pcdiv  12868  pcqcl  12872  pcexp  12875  pcdvds  12881  pcndvds  12883  pcndvds2  12885  pcelnn  12887  pcgcd1  12894  pc2dvds  12896  pc11  12897  gzsubcl  12946  4sqlem3  12956  setsresg  13113  pwssnf1o  13374  xpsfeq  13421  submcl  13555  grpinvnzcl  13648  mulgnnass  13737  nmzsubg  13790  nmznsg  13793  resghm2b  13842  ghmnsgpreima  13849  gsumfzsnfd  13925  iscrng2  14021  subrngpropd  14223  issubrg3  14254  subrgpropd  14260  islmodd  14300  lss1d  14390  lspsncl  14399  lspsnid  14414  df2idl2  14516  2idlcpbl  14531  qusrhm  14535  gsumfzfsumlemm  14594  iunopn  14719  unopn  14722  eltg  14769  eltg2  14770  tgcl  14781  tgiun  14790  tgidm  14791  isopn3i  14852  isneip  14863  neipsm  14871  restbasg  14885  restopn2  14900  lmbrf  14932  cnclima  14940  lmss  14963  txbasval  14984  txlm  14996  psmetxrge0  15049  blininf  15141  blssps  15144  blss  15145  elmopn2  15166  bdmet  15219  metrest  15223  bl2ioo  15267  dvcjbr  15425  plyaddlem1  15464  plymullem1  15465  plyreres  15481  dvply1  15482  dvply2g  15483  efper  15524  sinperlem  15525  abssinper  15563  cxpexprp  15612  logcxp  15614  rpcxpcl  15620  rpcxproot  15631  rprelogbmulexp  15673  lgsval2lem  15732  lgssq2  15763  lgsprme0  15764  ausgrusgrben  16012  bj-inex  16452  peano5set  16485  findset  16490  bj-findis  16524  nninfsellemsuc  16564  nninfself  16565  cvgcmp2nlemabs  16586  iooref1o  16588  trilpolemeq1  16594  nconstwlpolemgt0  16618