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  2944  sbciegft  3059  csbtt  3136  csbnestgf  3177  copsex2t  4330  pofun  4400  onsucmin  4596  onsucelsucr  4597  onsucsssucr  4598  ordsucunielexmid  4620  ordsuc  4652  nlimsucg  4655  elnn  4695  xpsspw  4828  elxp4  5212  elxp5  5213  funimass2  5395  imain  5399  funimaexg  5401  f1ff1  5535  dff1o2  5573  resdif  5590  funbrfv  5664  fvelimab  5683  eqfnfv2  5726  fvimacnvi  5742  ffvresb  5791  fnressn  5818  fmptapd  5823  fnex  5854  rexima  5871  ralima  5872  f1elima  5890  fnotovb  6038  mpoeq12  6055  fovcdm  6139  fnovrn  6144  ofrfval  6217  ofvalg  6218  cofunexg  6244  cofunex2g  6245  mpoexxg  6346  mpoexg  6347  f1o2ndf1  6364  spc2ed  6369  smodm2  6431  tfrlem9  6455  tfrlemibxssdm  6463  tfr1onlembxssdm  6479  tfrcllembxssdm  6492  tfri3  6503  rdgtfr  6510  rdgruledefgg  6511  oav2  6599  oasuc  6600  omv2  6601  onasuc  6602  omsuc  6608  onmsuc  6609  nnaass  6621  nndi  6622  nndir  6626  nnaword  6647  ecelqsg  6725  iinerm  6744  ecovass  6781  ecoviass  6782  ecovdi  6783  ecovidi  6784  fvdiagfn  6830  ixpssmap2g  6864  domentr  6933  xpdom1g  6980  fopwdom  6985  ssenen  7000  phplem3  7003  phplem4  7004  php5dom  7012  ssfilem  7025  diffitest  7037  ctssdccl  7266  pm54.43  7351  pw1if  7398  addclpi  7502  addasspig  7505  mulasspig  7507  distrpig  7508  mulcanpig  7510  nnppipi  7518  enqdc1  7537  addassnqg  7557  ltbtwnnqq  7590  prarloclemarch  7593  prarloclemarch2  7594  enq0sym  7607  enq0ref  7608  addclnq0  7626  nqpnq0nq  7628  nnanq0  7633  distrnq0  7634  addassnq0lemcl  7636  addassnq0  7637  distnq0r  7638  prarloclemlt  7668  genpassl  7699  genpassu  7700  genpassg  7701  nqpru  7727  addcomprg  7753  mulcomprg  7755  distrlem1prl  7757  distrlem1pru  7758  1idprl  7765  1idpru  7766  recexprlemdisj  7805  recexprlem1ssl  7808  peano2nnnn  8028  ax1rid  8052  axcaucvglemcl  8070  le2tri3i  8243  add4  8295  cnegexlem1  8309  cnegexlem3  8311  cnegex  8312  subadd  8337  addsub  8345  addsubeq4  8349  negdi  8391  renegcl  8395  resubcl  8398  subdi  8519  mulneg2  8530  mul2neg  8532  submul2  8533  ltnegcon2  8599  lenegcon2  8602  lesub0  8614  cru  8737  recextlem1  8786  recexap  8788  div12ap  8829  divnegap  8841  letrp1  8983  dfinfre  9091  peano2nn  9110  nndivre  9134  nnsub  9137  nndivtr  9140  arch  9354  bndndx  9356  nn0addge1  9403  nn0addge2  9404  zaddcl  9474  zsubcl  9475  zltnle  9480  zrevaddcl  9485  nzadd  9487  zleltp1  9490  zltlem1  9492  zdiv  9523  peano2uz2  9542  uzind  9546  eluzp1l  9735  ublbneg  9796  qaddcl  9818  qsubcl  9821  qreccl  9825  qdivcl  9826  qrevaddcl  9827  irradd  9829  irrmul  9830  rerpdivcl  9868  nn0ledivnn  9951  xrre  10004  rexsub  10037  xaddass  10053  xnpcan  10056  xsubge0  10065  xposdif  10066  elioc2  10120  icoshft  10174  iccdil  10182  fzss2  10248  fzsuc2  10263  fzrev2  10269  elfzm11  10275  elfzp1b  10281  fzrevral  10289  fzshftral  10292  fzof  10328  fzoval  10332  fzon  10351  elfzoextl  10384  fzosubel  10387  zpnn0elfzo  10400  elfzom1b  10422  qltnle  10450  flqlt  10490  flqbi  10497  flqaddz  10504  fzofig  10641  seq3feq2  10685  ser3le  10746  expp1  10755  expm1t  10776  expeq0  10779  binom2sub  10862  bernneq  10869  expnlbnd  10873  zzlesq  10917  faccl  10944  facdiv  10947  bcpasc  10975  bccl  10976  ffz0hash  11042  fnfzo0hash  11044  wrdlen1  11095  wrdred1  11100  ccatval21sw  11126  wrdl1exs1  11148  ccatws1cl  11151  ccatws1leng  11153  pfxmpt  11198  pfxfv  11202  pfxfvlsw  11213  ccatpfx  11219  pfx1  11221  swrdccatin1  11243  swrdccat  11253  pfxccatpfx1  11254  2shfti  11328  crim  11355  mulreap  11361  resub  11367  imsub  11375  ipcnval  11383  cjsub  11389  resqrexlemfp1  11506  resqrexlemgt0  11517  sqabsadd  11552  sqabssub  11553  abs2dif2  11604  cau3lem  11611  icodiamlt  11677  xrmaxaddlem  11757  clim  11778  clim2  11780  clim2c  11781  clim0c  11783  2clim  11798  climabs0  11804  climcn1  11805  climcn2  11806  climsqz  11832  climsqz2  11833  climub  11841  climserle  11842  fsum3cvg  11875  fisumss  11889  fsum3ser  11894  sumsplitdc  11929  fsump1i  11930  fsumlessfi  11957  telfsumo  11963  fsumparts  11967  iserabs  11972  binomlem  11980  isumsplit  11988  isum1p  11989  isumlessdc  11993  mertenslem2  12033  mertensabs  12034  prodfap0  12042  prodfrecap  12043  prodfdivap  12044  fproddccvg  12069  prodmodclem2  12074  fprodssdc  12087  fprodabs  12113  fprodeq0  12114  fprodeq0g  12135  ege2le3  12168  efsub  12178  efexp  12179  efsep  12188  sinsub  12237  cossub  12238  demoivre  12270  eirraplem  12274  moddvds  12296  0dvds  12308  iddvdsexp  12312  dvdssub  12335  dvdsle  12341  dvdsleabs  12342  dvdseq  12345  dvdsflip  12348  mulsucdiv2z  12382  divalgb  12422  divalg2  12423  ndvdsadd  12428  bitsp1  12448  gcdneg  12489  gcdabs2  12497  modgcd  12498  bezoutlemsup  12516  gcdmultiplez  12528  gcdeq  12530  dvdssq  12538  lcmcllem  12575  lcmneg  12582  lcmdvds  12587  qredeu  12605  cncongrcoprm  12614  isprm3  12626  prmrp  12653  divnumden  12704  phiprmpw  12730  crth  12732  hashgcdlem  12746  hashgcdeq  12748  modprminv  12758  modprminveq  12759  modprmn0modprm0  12765  coprimeprodsq2  12767  pcpre1  12801  pccl  12808  pcmul  12810  pcdiv  12811  pcqcl  12815  pcexp  12818  pcdvds  12824  pcndvds  12826  pcndvds2  12828  pcelnn  12830  pcgcd1  12837  pc2dvds  12839  pc11  12840  gzsubcl  12889  4sqlem3  12899  setsresg  13056  pwssnf1o  13317  xpsfeq  13364  submcl  13498  grpinvnzcl  13591  mulgnnass  13680  nmzsubg  13733  nmznsg  13736  resghm2b  13785  ghmnsgpreima  13792  gsumfzsnfd  13868  iscrng2  13964  subrngpropd  14165  issubrg3  14196  subrgpropd  14202  islmodd  14242  lss1d  14332  lspsncl  14341  lspsnid  14356  df2idl2  14458  2idlcpbl  14473  qusrhm  14477  gsumfzfsumlemm  14536  iunopn  14661  unopn  14664  eltg  14711  eltg2  14712  tgcl  14723  tgiun  14732  tgidm  14733  isopn3i  14794  isneip  14805  neipsm  14813  restbasg  14827  restopn2  14842  lmbrf  14874  cnclima  14882  lmss  14905  txbasval  14926  txlm  14938  psmetxrge0  14991  blininf  15083  blssps  15086  blss  15087  elmopn2  15108  bdmet  15161  metrest  15165  bl2ioo  15209  dvcjbr  15367  plyaddlem1  15406  plymullem1  15407  plyreres  15423  dvply1  15424  dvply2g  15425  efper  15466  sinperlem  15467  abssinper  15505  cxpexprp  15554  logcxp  15556  rpcxpcl  15562  rpcxproot  15573  rprelogbmulexp  15615  lgsval2lem  15674  lgssq2  15705  lgsprme0  15706  ausgrusgrben  15951  bj-inex  16200  peano5set  16233  findset  16238  bj-findis  16272  nninfsellemsuc  16309  nninfself  16310  cvgcmp2nlemabs  16331  iooref1o  16333  trilpolemeq1  16339  nconstwlpolemgt0  16363