Theorem sylan2b 606

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 219	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 605	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anb  610  eupickb  2663  2eu1  2678  2eu1v  2679  elnelne1  3076  elnelne2  3077  morex  3680  psssstr  4040  reuss2  4274  reupick  4277  reximdva0  4306  falseral0OLD  4474  rabsneu  4692  invdisjrab  5095  opabss  5175  triun  5233  triin  5235  poirr  5578  wefrc  5652  xpcan  6186  fnfco  6777  eqfnun  7067  fnressn  7194  fvtp3  7233  fvtp3g  7236  f1mpt  7296  offval  7734  ordsucuniel  7869  onzsl  7891  soex  7967  fiunlem  7988  fiun  7989  f1iun  7990  dfoprab3  8100  poxp  8177  fnwelem  8180  poxp2  8197  suppssr  8250  suppssrg  8251  suppsssn  8256  suppofssd  8258  fprlem2  8357  oeordsuc  8641  oelim2  8642  omsmolem  8704  ssnnfi  9223  ssfi  9226  ensymfib  9237  domnsymfi  9253  fiint  9356  unifi  9371  indexfi  9387  iinfi  9446  unwdomg  9615  inf3lem5  9670  rankr1bg  9848  rankr1c  9867  elhf4  9949  carden2a  10084  dfac8clem  10150  dfac5lem4  10244  pwsdompw  10320  cfsuc  10374  cflim2  10380  enfin2i  10438  isf34lem4  10494  axdc4lem  10572  zornn0g  10622  uniimadomf  10668  fpwwe2lem7  10761  fpwwe2lem11  10765  fpwwe2lem12  10766  pwfseqlem1  10782  pwfseqlem5  10787  intgru  10938  addclpi  11016  addnidpi  11025  ltsonq  11093  nqpr  11138  reclem3pr  11173  recexsr  11231  supsrlem  11235  nnnn0addcl  12676  un0addcl  12679  un0mulcl  12680  nn0nndivcl  12718  nn0ge0div  12808  uzind3  12833  uzind4  13073  zsupss  13104  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  ltsubrp  13198  ltaddrp  13199  xrlttr  13309  qbtwnxr  13370  xltnegi  13386  xaddnemnf  13406  xaddnepnf  13407  xaddcom  13410  xnegdi  13418  xsubge0  13431  xrub  13482  fzne1  13778  fzind2  13963  seqof  14242  expp1  14251  expneg  14252  expcllem  14255  mulexpz  14285  expaddz  14289  expmulz  14291  faclbnd4lem3  14480  faclbnd4  14482  fi1uzind  14693  swrd00  14834  swrd0  14850  cats1un  14912  reuccatpfxs1  14938  cshw0  14987  cshwn  14990  wwlktovfo  15154  shftf  15275  sqrtdiv  15475  leabs  15509  mulcn2  15807  summolem2  15926  fsumrev2  15992  geomulcvg  16089  prodmolem2  16146  zprod  16148  prodsn  16173  prodsnf  16175  fprodle  16207  bpolydiflem  16264  bpoly2  16267  bpoly3  16268  ruclem6  16447  dvdsflip  16531  dvdsfac  16540  gcdcllem1  16713  lcmgcdlem  16825  rpexp1i  16943  hashdvds  16996  hashgcdlem  17009  phisum  17012  iserodd  17057  pcqcl  17078  pcid  17095  ismred  17822  funcpropd  18127  natpropd  18204  odupos  18550  lubun  18739  rabsubmgmd  18943  sgrpidmnd  18978  issubmd  19051  grpinvnzcl  19271  mulgneg  19352  mulgnn0z  19361  symgfixf1  19702  symgsssg  19732  symgfisg  19733  pgpssslw  19879  sylow2alem2  19883  sylow2a  19884  oddvdssubg  20120  gsumzunsnd  20221  gsumunsnfd  20222  gsum2dlem1  20235  gsum2dlem2  20236  gsumcom3  20243  ablfac1eu  20340  pgpfac1lem5  20346  gsumdixp  20599  dvdsrcl2  20647  01eq0ring  20832  isdrng3lem1  21056  isdrng3lem2  21057  isdrngd  21073  isdrngdOLD  21075  unichnlidl  21567  isprmidlc  21679  ssdifidllem  21691  ssdifidlprm  21693  cnsubrg  21787  psgnodpm  21949  evlslem4  22440  psdmul  22542  coe1tmmul2  22650  mpomatmul  22816  matunitlindflem1  23049  cpmidpmat  23246  intcld  23413  neiptopnei  23505  ordtrest2lem  23576  lmss  23671  cmpcovf  23764  cncmp  23765  fincmp  23766  cmpsublem  23772  cmpsub  23773  unconn  23802  1stcfb  23818  2ndcsep  23833  refun0  23889  locfincmp  23900  1stckgenlem  23927  ptbasin  23951  ptbasfi  23955  ptunimpt  23969  ptuniconst  23972  dfac14  23992  ptcnp  23996  xkoptsub  24028  xkococnlem  24033  xkoinjcn  24061  qtopcmplem  24081  qtophmeo  24191  fbfinnfr  24215  isufil2  24282  isfcls  24383  xmetrtri  24729  xmetrtri2  24730  blssioo  25169  divcn  25244  bndth  25334  clmvscom  25466  resscdrg  25734  minveclem3  25805  finiunmbl  25920  opnmbllem  25977  ismbf2d  26016  itg2seq  26118  bddiblnc  26217  ellimc2  26252  limcmpt2  26259  limcres  26261  dvlem  26271  dvidlem  26290  dvrec  26330  dveflem  26354  dvlip  26368  coe1mul3  26472  rngunsnply  26693  dvtaylp  26754  leibpilem2  27326  leibpi  27327  wilthlem2  27453  basellem3  27467  dchreq  27642  dchrsum  27653  lgsval3  27699  lgsdir2lem4  27712  2sqlem6  27807  rpvmasumlem  27871  dchrisum0fno1  27895  rpvmasum2  27896  pntrsumbnd2  27951  ostthlem1  28011  infdesc  28024  nosupno  28117  negbdaylem  28499  expsp1  28872  colmid  29217  plngrotlem2  29323  lmiisolem  29358  dfcgra2  29395  prlngmolem2  29488  axcontlem2  29600  axcontlem7  29605  upgrex  29727  umgredg  29773  umgrpredgv  29775  umgredgne  29780  umgredgnlp  29782  usgredgppr  29834  edgssv2  29836  uspgredg2vlem  29861  usgredg2vlem1  29863  upgrres1  29951  nbuhgr2vtx1edgblem  29989  nbusgrf1o0  30007  hashnbusgrnn0  30014  iscplgredg  30055  uhgrvd00  30172  finsumvtxdg2size  30188  wlkepvtx  30296  wlknewwlksn  30533  wwlksnextfun  30544  wwlksnextsurj  30546  elwwlks2ons3im  30600  wwlks2onsym  30606  clwwlkf  30695  fusgreghash2wspv  30993  numclwwlk5lem  31045  grpoidinvlem3  31165  ablo32  31208  ablomuldiv  31211  ablodivdiv  31212  ablodiv32  31214  nvscom  31288  dipassr  31505  htthlem  31576  hsn0elch  31907  shscli  31976  nmopun  32673  branmfn  32764  mdslj1i  32978  mdslj2i  32979  atss  33005  chcv1  33014  dmdbr5ati  33081  snsssng  33209  ifnebib  33243  fnpreimac  33362  fcnvgreu  33364  isoun  33392  fsuppcurry1  33412  fsuppcurry2  33413  prodpr  33513  prodtp  33514  pmtrprfv2  33748  elrgspnsubrunlem2  33908  nsgmgclem  34066  nsgqusf1olem2  34069  ssmxidllem  34102  qsdrng  34125  1arithufdlem3  34182  ordtrest2NEWlem  34665  esumsplit  34796  esumpad2  34799  esumpcvgval  34821  sigaclcu2  34863  ldgenpisyslem1  34907  volmeas  34975  mbfmco2  35008  omsmeas  35066  oddpwdc  35097  eulerpartlemgvv  35119  ballotlemfc0  35236  ballotlemfcc  35237  prodfzo03  35343  circlemethhgt  35383  bnj1109  35528  bnj1294  35558  bnj545  35636  bnj605  35648  bnj594  35653  bnj934  35676  bnj953  35680  bnj1137  35736  bnj1174  35744  bnj1388  35774  jltaleph  36067  vonf1oonfo  36090  subfacp1lem4  36156  erdszelem7  36170  erdszelem8  36171  erdsze2lem2  36177  resconn  36219  cvmsdisj  36243  cvmscld  36246  satf0op  36350  mclsax  36542  climuzcnv  36644  pocnv  36743  cgrid2  36983  btwncom  36994  btwnswapid2  36998  colinearperm1  37042  colinearperm3  37043  colinearperm2  37044  colinearperm4  37045  lineext  37056  colinbtwnle  37098  broutsideof2  37102  outsideofcom  37108  linecom  37130  linerflx2  37131  lineintmo  37137  fwddifn0  37144  hfext  37149  nmulel1  37179  ntruni  37330  clsint2  37332  neibastop1  37362  weiunlem  37466  bj-snsetex  38091  relowlssretop  38554  pibt2  38608  fin2solem  38797  lindsadd  38804  poimirlem4  38810  poimirlem25  38831  poimirlem32  38838  opnmbllem0  38842  mblfinlem3  38845  mbfposadd  38853  itg2addnclem3  38859  ftc1anclem6  38884  ftc1anc  38887  ac6gf  38934  heibor1lem  39009  isdrngo2  39158  unichnidl  39231  isfldidl  39268  cnf1dd  39288  membpartlem19  40112  lkrss2N  40492  elpadd0  41132  ltrnu  41444  tendoex  42298  cdlemm10N  42441  dicfnN  42506  dihmeetlem2N  42622  dihlatat  42660  lcfrlem9  42873  uzindd  43294  sticksstones1  43462  ofun  43556  nn0addcom  43792  nn0mulcom  43796  zmulcomlem  43797  fsuppind  43884  ismrcd1  43975  isnacs3  43987  pellfundglb  44158  jm2.22  44268  jm2.23  44269  isnumbasgrplem1  44368  hbtlem6  44396  ordsssucim  44665  mnringmulrcld  45487  dvgrat  45557  cvgdvgrat  45558  nznngen  45561  uzmptshftfval  45591  wfac8prim  46256  rnmptlb  46528  rnmptbddlem  46529  rnmptbd2lem  46533  iccshift  46803  iooshift  46807  liminflbuz2  47098  xlimbr  47110  itgperiod  47264  fourierdlem42  47432  fourierdlem68  47457  fourierdlem93  47482  smfpimne2  48123  elprneb  48372  dfatcolem  48598  modmknepk  48711  ichim  48812  ichnfb  48820  prproropf1olem1  48858  prproropf1olem3  48860  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  2zlidl  49610  lspsslco  49880  isthincd2  50903  fullthinc  50916