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  436  adantrl  475  adantrr  476  ancom2s  561  3adantr1  1151  3adantr2  1152  3adantr3  1153  syl3anr1  1285  syl3anr3  1287  dfbi3dc  1392  xordidc  1394  elabgt  2871  sbciegft  2985  csbtt  3061  csbnestgf  3101  copsex2t  4228  pofun  4295  onsucmin  4489  onsucelsucr  4490  onsucsssucr  4491  ordsucunielexmid  4513  ordsuc  4545  nlimsucg  4548  elnn  4588  xpsspw  4721  elxp4  5096  elxp5  5097  funimass2  5274  imain  5278  funimaexg  5280  f1ff1  5409  dff1o2  5445  resdif  5462  funbrfv  5533  fvelimab  5550  eqfnfv2  5592  fvimacnvi  5607  ffvresb  5656  fnressn  5679  fmptapd  5684  fnex  5715  rexima  5731  ralima  5732  f1elima  5749  fnotovb  5893  mpoeq12  5910  fovrn  5992  fnovrn  5997  ofrfval  6066  ofvalg  6067  cofunexg  6085  cofunex2g  6086  mpoexxg  6186  mpoexg  6187  f1o2ndf1  6204  spc2ed  6209  smodm2  6271  tfrlem9  6295  tfrlemibxssdm  6303  tfr1onlembxssdm  6319  tfrcllembxssdm  6332  tfri3  6343  rdgtfr  6350  rdgruledefgg  6351  oav2  6439  oasuc  6440  omv2  6441  onasuc  6442  omsuc  6448  onmsuc  6449  nnaass  6461  nndi  6462  nndir  6466  nnaword  6487  ecelqsg  6562  iinerm  6581  ecovass  6618  ecoviass  6619  ecovdi  6620  ecovidi  6621  fvdiagfn  6667  ixpssmap2g  6701  domentr  6765  xpdom1g  6807  fopwdom  6810  ssenen  6825  phplem3  6828  phplem4  6829  php5dom  6837  ssfilem  6849  diffitest  6861  ctssdccl  7084  pm54.43  7154  addclpi  7276  addasspig  7279  mulasspig  7281  distrpig  7282  mulcanpig  7284  nnppipi  7292  enqdc1  7311  addassnqg  7331  ltbtwnnqq  7364  prarloclemarch  7367  prarloclemarch2  7368  enq0sym  7381  enq0ref  7382  addclnq0  7400  nqpnq0nq  7402  nnanq0  7407  distrnq0  7408  addassnq0lemcl  7410  addassnq0  7411  distnq0r  7412  prarloclemlt  7442  genpassl  7473  genpassu  7474  genpassg  7475  nqpru  7501  addcomprg  7527  mulcomprg  7529  distrlem1prl  7531  distrlem1pru  7532  1idprl  7539  1idpru  7540  recexprlemdisj  7579  recexprlem1ssl  7582  peano2nnnn  7802  ax1rid  7826  axcaucvglemcl  7844  le2tri3i  8015  add4  8067  cnegexlem1  8081  cnegexlem3  8083  cnegex  8084  subadd  8109  addsub  8117  addsubeq4  8121  negdi  8163  renegcl  8167  resubcl  8170  subdi  8291  mulneg2  8302  mul2neg  8304  submul2  8305  ltnegcon2  8370  lenegcon2  8373  lesub0  8385  cru  8508  recextlem1  8556  recexap  8558  div12ap  8598  divnegap  8610  letrp1  8751  dfinfre  8859  peano2nn  8877  nndivre  8901  nnsub  8904  nndivtr  8907  arch  9119  bndndx  9121  nn0addge1  9168  nn0addge2  9169  zaddcl  9239  zsubcl  9240  zltnle  9245  zrevaddcl  9249  nzadd  9251  zleltp1  9254  zltlem1  9256  zdiv  9287  peano2uz2  9306  uzind  9310  eluzp1l  9498  ublbneg  9559  qaddcl  9581  qsubcl  9584  qreccl  9588  qdivcl  9589  qrevaddcl  9590  irradd  9592  irrmul  9593  rerpdivcl  9628  nn0ledivnn  9711  xrre  9764  rexsub  9797  xaddass  9813  xnpcan  9816  xsubge0  9825  xposdif  9826  elioc2  9880  icoshft  9934  iccdil  9942  fzss2  10007  fzsuc2  10022  fzrev2  10028  elfzm11  10034  elfzp1b  10040  fzrevral  10048  fzshftral  10051  fzof  10087  fzoval  10091  fzon  10109  fzosubel  10137  zpnn0elfzo  10150  elfzom1b  10172  qltnle  10189  flqlt  10226  flqbi  10233  flqaddz  10240  fzofig  10375  seq3feq2  10413  ser3le  10461  expp1  10470  expm1t  10491  expeq0  10494  binom2sub  10576  bernneq  10583  expnlbnd  10587  faccl  10656  facdiv  10659  bcpasc  10687  bccl  10688  ffz0hash  10755  fnfzo0hash  10757  2shfti  10782  crim  10809  mulreap  10815  resub  10821  imsub  10829  ipcnval  10837  cjsub  10843  resqrexlemfp1  10960  resqrexlemgt0  10971  sqabsadd  11006  sqabssub  11007  abs2dif2  11058  cau3lem  11065  icodiamlt  11131  xrmaxaddlem  11210  clim  11231  clim2  11233  clim2c  11234  clim0c  11236  2clim  11251  climabs0  11257  climcn1  11258  climcn2  11259  climsqz  11285  climsqz2  11286  climub  11294  climserle  11295  fsum3cvg  11328  fisumss  11342  fsum3ser  11347  sumsplitdc  11382  fsump1i  11383  fsumlessfi  11410  telfsumo  11416  fsumparts  11420  iserabs  11425  binomlem  11433  isumsplit  11441  isum1p  11442  isumlessdc  11446  mertenslem2  11486  mertensabs  11487  prodfap0  11495  prodfrecap  11496  prodfdivap  11497  fproddccvg  11522  prodmodclem2  11527  fprodssdc  11540  fprodabs  11566  fprodeq0  11567  fprodeq0g  11588  ege2le3  11621  efsub  11631  efexp  11632  efsep  11641  sinsub  11690  cossub  11691  demoivre  11722  eirraplem  11726  moddvds  11748  0dvds  11760  iddvdsexp  11764  dvdssub  11787  dvdsle  11791  dvdsleabs  11792  dvdseq  11795  dvdsflip  11798  mulsucdiv2z  11831  divalgb  11871  divalg2  11872  ndvdsadd  11877  gcdneg  11924  gcdabs2  11932  modgcd  11933  bezoutlemsup  11951  gcdmultiplez  11963  gcdeq  11965  dvdssq  11973  lcmcllem  12008  lcmneg  12015  lcmdvds  12020  qredeu  12038  cncongrcoprm  12047  isprm3  12059  prmrp  12086  divnumden  12137  phiprmpw  12163  crth  12165  hashgcdlem  12179  hashgcdeq  12180  modprminv  12190  modprminveq  12191  modprmn0modprm0  12197  coprimeprodsq2  12199  pcpre1  12233  pccl  12240  pcmul  12242  pcdiv  12243  pcqcl  12247  pcexp  12250  pcdvds  12255  pcndvds  12257  pcndvds2  12259  pcelnn  12261  pcgcd1  12268  pc2dvds  12270  pc11  12271  gzsubcl  12319  4sqlem3  12329  setsresg  12441  submcl  12687  iunopn  12715  unopn  12718  eltg  12767  eltg2  12768  tgcl  12779  tgiun  12788  tgidm  12789  isopn3i  12850  isneip  12861  neipsm  12869  restbasg  12883  restopn2  12898  lmbrf  12930  cnclima  12938  lmss  12961  txbasval  12982  txlm  12994  psmetxrge0  13047  blininf  13139  blssps  13142  blss  13143  elmopn2  13164  bdmet  13217  metrest  13221  bl2ioo  13257  dvcjbr  13387  efper  13443  sinperlem  13444  abssinper  13482  cxpexprp  13531  logcxp  13533  rpcxpcl  13539  rpcxproot  13549  rprelogbmulexp  13589  lgsval2lem  13626  lgssq2  13657  lgsprme0  13658  bj-inex  13864  peano5set  13897  findset  13902  bj-findis  13936  nninfsellemsuc  13967  nninfself  13968  cvgcmp2nlemabs  13986  iooref1o  13988  trilpolemeq1  13994  nconstwlpolemgt0  14017