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 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  408  sylanr2  409  mpanr2  442  adantrl  482  adantrr  483  ancom2s  572  annimdc  950  ifpnst  1001  3adantr1  1187  3adantr2  1188  3adantr3  1189  syl3anr1  1330  syl3anr3  1332  dfbi3dc  1446  xordidc  1448  elabgt  2967  sbciegft  3082  csbtt  3159  csbnestgf  3200  copsex2t  4385  pofun  4457  onsucmin  4654  onsucelsucr  4655  onsucsssucr  4656  ordsucunielexmid  4678  ordsuc  4710  nlimsucg  4713  elnn  4753  xpsspw  4887  elxp4  5275  elxp5  5276  funimass2  5459  imain  5463  funimaexg  5465  f1ff1  5606  dff1o2  5644  resdif  5661  funbrfv  5739  fnbrfvb2  5745  fvelimab  5759  eqfnfv2  5807  fvimacnvi  5823  ffvresb  5871  fnressn  5901  fmptapd  5906  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fnotovb  6131  mpoeq12  6148  fovcdm  6232  fnovrn  6237  ofrfval  6311  ofvalg  6312  cofunexg  6338  cofunex2g  6339  mpoexxg  6446  mpoexg  6447  f1o2ndf1  6464  spc2ed  6469  funsssuppss  6498  smodm2  6566  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  oav2  6736  oasuc  6737  omv2  6738  onasuc  6739  omsuc  6745  onmsuc  6746  nnaass  6758  nndi  6759  nndir  6763  nnaword  6784  ecelqsg  6862  iinerm  6881  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  fvdiagfn  6975  ixpssmap2g  7009  domentr  7078  xpdom1g  7131  fopwdom  7136  ssenen  7152  phplem3  7155  phplem4  7156  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  ctssdccl  7452  pm54.43  7537  pw1if  7585  addclpi  7695  addasspig  7698  mulasspig  7700  distrpig  7701  mulcanpig  7703  nnppipi  7711  enqdc1  7730  addassnqg  7750  ltbtwnnqq  7783  prarloclemarch  7786  prarloclemarch2  7787  enq0sym  7800  enq0ref  7801  addclnq0  7819  nqpnq0nq  7821  nnanq0  7826  distrnq0  7827  addassnq0lemcl  7829  addassnq0  7830  distnq0r  7831  prarloclemlt  7861  genpassl  7892  genpassu  7893  genpassg  7894  nqpru  7920  addcomprg  7946  mulcomprg  7948  distrlem1prl  7950  distrlem1pru  7951  1idprl  7958  1idpru  7959  recexprlemdisj  7998  recexprlem1ssl  8001  peano2nnnn  8221  ax1rid  8245  axcaucvglemcl  8263  le2tri3i  8436  add4  8489  cnegexlem1  8503  cnegexlem3  8505  cnegex  8506  subadd  8531  addsub  8539  addsubeq4  8543  negdi  8585  renegcl  8589  resubcl  8592  subdi  8714  mulneg2  8725  mul2neg  8727  submul2  8728  ltnegcon2  8794  lenegcon2  8797  lesub0  8809  cru  8933  recextlem1  8982  recexap  8984  div12ap  9027  divnegap  9039  letrp1  9181  dfinfre  9289  peano2nn  9319  nndivre  9343  nnsub  9346  nndivtr  9349  arch  9565  bndndx  9567  nn0addge1  9614  nn0addge2  9615  zaddcl  9689  zsubcl  9690  zltnle  9695  zrevaddcl  9700  nzadd  9702  zleltp1  9705  zltlem1  9707  zdiv  9739  peano2uz2  9758  uzind  9762  eluzp1l  9957  ublbneg  10023  qaddcl  10045  qsubcl  10048  qreccl  10052  qdivcl  10053  qrevaddcl  10054  irradd  10056  irrmul  10058  rerpdivcl  10096  nn0ledivnn  10179  xrre  10233  rexsub  10266  xaddass  10282  xnpcan  10285  xsubge0  10294  xposdif  10295  elioc2  10349  icoshft  10403  iccdil  10411  fzss2  10481  fzsuc2  10497  fzrev2  10503  elfzm11  10509  elfzp1b  10515  fzrevral  10523  fzshftral  10526  fzof  10562  fzoval  10566  fzon  10585  elfzoextl  10620  fzosubel  10623  zpnn0elfzo  10636  elfzom1b  10658  qltnle  10689  flapcl  10722  flaplelt  10724  flqlt  10732  flqbi  10739  flqaddz  10746  fzofig  10883  seq3feq2  10927  ser3le  10988  expp1  10997  expm1t  11018  expeq0  11021  binom2sub  11104  bernneq  11112  expnlbnd  11116  zzlesq  11160  faccl  11188  facdiv  11191  bcpasc  11219  bccl  11220  ffz0hash  11291  fnfzo0hash  11293  hashfibclem  11297  hashf1lem2  11301  wrdlen1  11357  wrdred1  11362  ccatval21sw  11388  wrdl1exs1  11412  ccatws1cl  11415  ccatws1leng  11417  pfxmpt  11467  pfxfv  11471  pfxfvlsw  11482  ccatpfx  11488  pfx1  11490  swrdccatin1  11512  swrdccat  11522  pfxccatpfx1  11523  2shfti  11611  crim  11638  mulreap  11644  resub  11650  imsub  11658  ipcnval  11666  cjsub  11672  resqrexlemfp1  11790  resqrexlemgt0  11801  sqabsadd  11836  sqabssub  11837  abs2dif2  11889  cau3lem  11896  icodiamlt  11962  xrmaxaddlem  12044  clim  12065  clim2  12067  clim2c  12068  clim0c  12070  2clim  12085  climabs0  12091  climcn1  12092  climcn2  12093  climsqz  12119  climsqz2  12120  climub  12128  climserle  12129  fsum3cvg  12163  fisumss  12177  fsum3ser  12182  sumsplitdc  12217  fsump1i  12218  fsumlessfi  12245  telfsumo  12251  fsumparts  12255  iserabs  12260  binomlem  12268  isumsplit  12276  isum1p  12277  isumlessdc  12281  mertenslem2  12321  mertensabs  12322  prodfap0  12330  prodfrecap  12331  prodfdivap  12332  fproddccvg  12357  prodmodclem2  12362  fprodssdc  12375  fprodabs  12401  fprodeq0  12402  fprodeq0g  12423  ege2le3  12456  efsub  12466  efexp  12467  efsep  12476  sinsub  12525  cossub  12526  demoivre  12558  eirraplem  12562  moddvds  12584  0dvds  12596  iddvdsexp  12600  dvdssub  12623  dvdsle  12629  dvdsleabs  12630  dvdseq  12633  dvdsflip  12636  mulsucdiv2z  12670  divalgb  12710  divalg2  12711  ndvdsadd  12716  bitsp1  12736  gcdneg  12777  gcdabs2  12785  modgcd  12786  bezoutlemsup  12804  gcdmultiplez  12816  gcdeq  12818  dvdssq  12826  lcmcllem  12863  lcmneg  12870  lcmdvds  12875  qredeu  12893  cncongrcoprm  12902  isprm3  12914  prmrp  12942  divnumden  12994  phiprmpw  13022  crth  13024  hashgcdlem  13038  hashgcdeq  13040  modprminv  13050  modprminveq  13051  modprmn0modprm0  13057  coprimeprodsq2  13059  pcpre1  13093  pccl  13100  pcmul  13102  pcdiv  13103  pcqcl  13107  pcexp  13110  pcdvds  13116  pcndvds  13118  pcndvds2  13120  pcelnn  13122  pcgcd1  13129  pc2dvds  13131  pc11  13132  gzsubcl  13181  4sqlem3  13191  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemodife  13291  ballotfilemfrceq  13323  setsresg  13441  xpsfeq  13717  submcl  13837  grpinvnzcl  13928  mulgnnass  14011  nmzsubg  14064  nmznsg  14067  resghm2b  14116  ghmnsgpreima  14123  gzsumsnfd  14198  pwssnf1o  14262  iscrng2  14370  subrngpropd  14575  issubrg3  14606  subrgpropd  14612  islmodd  14680  lss1d  14771  lspsncl  14780  lspsnid  14795  df2idl2  14897  2idlcpbl  14912  qusrhm  14916  iunopn  15155  unopn  15158  eltg  15205  eltg2  15206  tgcl  15217  tgiun  15226  tgidm  15227  isopn3i  15288  isneip  15299  neipsm  15307  restbasg  15321  restopn2  15336  lmbrf  15368  cnclima  15376  lmss  15399  txbasval  15420  txlm  15432  psmetxrge0  15485  blininf  15577  blssps  15580  blss  15581  elmopn2  15602  bdmet  15655  metrest  15659  bl2ioo  15703  dvcjbr  15861  plyaddlem1  15900  plymullem1  15901  plyreres  15917  dvply1  15918  dvply2g  15919  efper  15961  sinperlem  15962  abssinper  16000  cxpexprp  16053  logcxp  16055  rpcxpcl  16061  rpcxproot  16072  rprelogbmulexp  16114  log2tlbndlog2  16142  prmorcht  16204  bposlem2  16234  lgsval2lem  16251  lgssq2  16282  lgsprme0  16283  ausgrusgrben  16531  wlkepvtx  16738  bj-inex  17055  peano5set  17088  findset  17093  bj-findis  17127  nninfsellemsuc  17177  nninfself  17178  cvgcmp2nlemabs  17203  iooref1o  17205  trilpolemeq1  17211  nconstwlpolemgt0  17236