Theorem sylan2b 594

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	⊢ (𝜑 ↔ 𝜒)
sylan2b.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2b	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 ⊢ (𝜑 ↔ 𝜒)
2	1	biimpi 216	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 593	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  syl2anb  598  eupickb  2628  2eu1  2644  2eu1v  2645  elnelne1  3040  elnelne2  3041  morex  3675  psssstr  4056  reuss2  4273  reupick  4276  reximdva0  4302  falseral0  4463  rabsneu  4679  invdisjrab  5075  opabss  5152  triun  5209  triin  5211  poirr  5533  wefrc  5607  xpcan  6119  fnfco  6683  eqfnun  6964  fnressn  7085  fvtp3  7125  fvtp3g  7128  f1mpt  7189  offval  7613  ordsucuniel  7748  onzsl  7770  soex  7845  fiunlem  7868  fiun  7869  f1iun  7870  dfoprab3  7980  poxp  8052  fnwelem  8055  poxp2  8067  suppssr  8119  suppssrg  8120  suppsssn  8125  suppofssd  8127  fprlem2  8225  oeordsuc  8503  oelim2  8504  omsmolem  8566  ssnnfi  9073  ssfi  9076  ensymfib  9087  domnsymfi  9103  fiint  9205  unifi  9222  indexfi  9238  iinfi  9295  unwdomg  9464  inf3lem5  9516  rankr1bg  9687  rankr1c  9705  carden2a  9850  dfac8clem  9914  dfac5lem4  10008  dfac5lem4OLD  10010  pwsdompw  10085  cfsuc  10139  cflim2  10145  enfin2i  10203  isf34lem4  10259  axdc4lem  10337  zornn0g  10387  uniimadomf  10427  fpwwe2lem7  10519  fpwwe2lem11  10523  fpwwe2lem12  10524  pwfseqlem1  10540  pwfseqlem5  10545  intgru  10696  addclpi  10774  addnidpi  10783  ltsonq  10851  nqpr  10896  reclem3pr  10931  recexsr  10989  supsrlem  10993  nnnn0addcl  12402  un0addcl  12405  un0mulcl  12406  nn0nndivcl  12444  nn0ge0div  12533  uzind3  12558  uzind4  12795  zsupss  12826  rpnnen1lem2  12866  rpnnen1lem1  12867  rpnnen1lem3  12868  rpnnen1lem5  12870  ltsubrp  12919  ltaddrp  12920  xrlttr  13030  qbtwnxr  13090  xltnegi  13106  xaddnemnf  13126  xaddnepnf  13127  xaddcom  13130  xnegdi  13138  xsubge0  13151  xrub  13202  fzne1  13495  fzind2  13676  seqof  13954  expp1  13963  expneg  13964  expcllem  13967  mulexpz  13997  expaddz  14001  expmulz  14003  faclbnd4lem3  14190  faclbnd4  14192  fi1uzind  14402  swrd00  14539  swrd0  14553  cats1un  14615  reuccatpfxs1  14641  cshw0  14688  cshwn  14691  wwlktovfo  14852  shftf  14973  sqrtdiv  15159  leabs  15193  mulcn2  15490  summolem2  15610  fsumrev2  15676  geomulcvg  15770  prodmolem2  15829  zprod  15831  prodsn  15856  prodsnf  15858  fprodle  15890  bpolydiflem  15948  bpoly2  15951  bpoly3  15952  ruclem6  16131  dvdsflip  16215  dvdsfac  16224  gcdcllem1  16397  lcmgcdlem  16504  rpexp1i  16621  hashdvds  16673  hashgcdlem  16686  phisum  16689  iserodd  16734  pcqcl  16755  pcid  16772  ismred  17491  funcpropd  17796  natpropd  17873  odupos  18219  lubun  18408  rabsubmgmd  18565  sgrpidmnd  18600  issubmd  18667  grpinvnzcl  18877  mulgneg  18958  mulgnn0z  18967  symgfixf1  19303  symgsssg  19333  symgfisg  19334  pgpssslw  19480  sylow2alem2  19484  sylow2a  19485  oddvdssubg  19721  gsumzunsnd  19822  gsumunsnfd  19823  gsum2dlem1  19836  gsum2dlem2  19837  gsumcom3  19844  ablfac1eu  19941  pgpfac1lem5  19947  gsumdixp  20191  dvdsrcl2  20238  01eq0ring  20399  isdrngd  20634  isdrngdOLD  20636  cnsubrg  21318  psgnodpm  21479  evlslem4  21965  psdmul  22035  coe1tmmul2  22144  mpomatmul  22315  cpmidpmat  22742  intcld  22909  neiptopnei  23001  ordtrest2lem  23072  lmss  23167  cmpcovf  23260  cncmp  23261  fincmp  23262  cmpsublem  23268  cmpsub  23269  unconn  23298  1stcfb  23314  2ndcsep  23328  refun0  23384  locfincmp  23395  1stckgenlem  23422  ptbasin  23446  ptbasfi  23450  ptunimpt  23464  ptuniconst  23467  dfac14  23487  ptcnp  23491  xkoptsub  23523  xkococnlem  23528  xkoinjcn  23556  qtopcmplem  23576  qtophmeo  23686  fbfinnfr  23710  isufil2  23777  isfcls  23878  xmetrtri  24224  xmetrtri2  24225  blssioo  24664  divcnOLD  24738  divcn  24740  bndth  24838  clmvscom  24971  resscdrg  25239  minveclem3  25310  finiunmbl  25426  opnmbllem  25483  ismbf2d  25522  itg2seq  25624  bddiblnc  25724  ellimc2  25759  limcmpt2  25766  limcres  25768  dvlem  25778  dvidlem  25797  dvrec  25840  dveflem  25864  dvlip  25879  coe1mul3  25985  dvtaylp  26259  leibpilem2  26832  leibpi  26833  wilthlem2  26960  basellem3  26974  dchreq  27150  dchrsum  27161  lgsval3  27207  lgsdir2lem4  27220  2sqlem6  27315  rpvmasumlem  27379  dchrisum0fno1  27403  rpvmasum2  27404  pntrsumbnd2  27459  ostthlem1  27519  nosupno  27596  negsbdaylem  27952  expsp1  28306  colmid  28620  lmiisolem  28728  dfcgra2  28762  axcontlem2  28897  axcontlem7  28902  upgrex  29024  umgredg  29070  umgrpredgv  29072  umgredgne  29077  umgredgnlp  29079  usgredgppr  29128  edgssv2  29130  uspgredg2vlem  29155  usgredg2vlem1  29157  upgrres1  29245  nbuhgr2vtx1edgblem  29283  nbusgrf1o0  29301  hashnbusgrnn0  29308  iscplgredg  29349  uhgrvd00  29467  finsumvtxdg2size  29483  wlkepvtx  29591  wlknewwlksn  29819  wwlksnextfun  29830  wwlksnextsurj  29832  elwwlks2ons3im  29886  wwlks2onsym  29890  clwwlkf  29978  fusgreghash2wspv  30266  numclwwlk5lem  30318  grpoidinvlem3  30437  ablo32  30480  ablomuldiv  30483  ablodivdiv  30484  ablodiv32  30486  nvscom  30560  dipassr  30777  htthlem  30848  hsn0elch  31179  shscli  31248  nmopun  31945  branmfn  32036  mdslj1i  32250  mdslj2i  32251  atss  32277  chcv1  32286  dmdbr5ati  32353  snsssng  32446  ifnebib  32481  fnpreimac  32605  fcnvgreu  32607  isoun  32635  fsuppcurry1  32659  fsuppcurry2  32660  prodpr  32764  prodtp  32765  pmtrprfv2  33025  elrgspnsubrunlem2  33183  nsgmgclem  33344  nsgqusf1olem2  33347  isprmidlc  33380  ssdifidllem  33389  ssdifidlprm  33391  ssmxidllem  33406  qsdrng  33430  1arithufdlem3  33479  ordtrest2NEWlem  33903  esumsplit  34034  esumpad2  34037  esumpcvgval  34059  sigaclcu2  34101  ldgenpisyslem1  34144  volmeas  34212  mbfmco2  34246  omsmeas  34304  oddpwdc  34335  eulerpartlemgvv  34357  ballotlemfc0  34474  ballotlemfcc  34475  prodfzo03  34584  circlemethhgt  34624  bnj1109  34766  bnj1294  34797  bnj545  34875  bnj605  34887  bnj594  34892  bnj934  34915  bnj953  34919  bnj1137  34975  bnj1174  34983  bnj1388  35013  subfacp1lem4  35173  erdszelem7  35187  erdszelem8  35188  erdsze2lem2  35194  resconn  35236  cvmsdisj  35260  cvmscld  35263  satf0op  35367  mclsax  35559  climuzcnv  35661  pocnv  35753  cgrid2  35994  btwncom  36005  btwnswapid2  36009  colinearperm1  36053  colinearperm3  36054  colinearperm2  36055  colinearperm4  36056  lineext  36067  colinbtwnle  36109  broutsideof2  36113  outsideofcom  36119  linecom  36141  linerflx2  36142  lineintmo  36148  fwddifn0  36155  hfext  36174  ntruni  36318  clsint2  36320  neibastop1  36350  weiunlem2  36454  bj-snsetex  36954  relowlssretop  37354  pibt2  37408  fin2solem  37603  lindsadd  37610  matunitlindflem1  37613  poimirlem4  37621  poimirlem25  37642  poimirlem32  37649  opnmbllem0  37653  mblfinlem3  37656  mbfposadd  37664  itg2addnclem3  37670  ftc1anclem6  37695  ftc1anc  37698  ac6gf  37729  heibor1lem  37806  isdrngo2  37955  unichnidl  38028  isfldidl  38065  cnf1dd  38087  membpartlem19  38806  lkrss2N  39165  elpadd0  39805  ltrnu  40117  tendoex  40971  cdlemm10N  41114  dicfnN  41179  dihmeetlem2N  41295  dihlatat  41333  lcfrlem9  41546  uzindd  41967  sticksstones1  42136  ofun  42226  nn0addcom  42452  nn0mulcom  42456  zmulcomlem  42457  fsuppind  42580  prjspner1  42616  infdesc  42633  ismrcd1  42688  isnacs3  42700  pellfundglb  42875  jm2.22  42985  jm2.23  42986  isnumbasgrplem1  43091  hbtlem6  43119  rngunsnply  43159  ordsssucim  43392  mnringmulrcld  44218  dvgrat  44302  cvgdvgrat  44303  nznngen  44306  uzmptshftfval  44336  wfac8prim  44992  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  iccshift  45515  iooshift  45519  liminflbuz2  45810  xlimbr  45822  itgperiod  45976  fourierdlem42  46144  fourierdlem68  46169  fourierdlem93  46194  smfpimne2  46835  elprneb  47027  dfatcolem  47253  modmknepk  47360  ichim  47455  ichnfb  47463  prproropf1olem1  47501  prproropf1olem3  47503  gpgnbgrvtx0  48072  gpgnbgrvtx1  48073  2zlidl  48238  lspsslco  48436  isthincd2  49436  fullthinc  49449