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  2660  2eu1  2675  2eu1v  2676  elnelne1  3072  elnelne2  3073  morex  3676  psssstr  4037  reuss2  4271  reupick  4274  reximdva0  4302  falseral0OLD  4470  rabsneu  4686  invdisjrab  5089  opabss  5168  triun  5226  triin  5228  poirr  5570  wefrc  5644  xpcan  6167  fnfco  6748  eqfnun  7037  fnressn  7163  fvtp3  7203  fvtp3g  7206  f1mpt  7266  offval  7703  ordsucuniel  7836  onzsl  7858  soex  7934  fiunlem  7955  fiun  7956  f1iun  7957  dfoprab3  8066  poxp  8143  fnwelem  8146  poxp2  8163  suppssr  8216  suppssrg  8217  suppsssn  8222  suppofssd  8224  fprlem2  8323  oeordsuc  8607  oelim2  8608  omsmolem  8670  ssnnfi  9189  ssfi  9192  ensymfib  9203  domnsymfi  9219  fiint  9322  unifi  9337  indexfi  9353  iinfi  9413  unwdomg  9582  inf3lem5  9637  rankr1bg  9815  rankr1c  9834  elhf4  9916  carden2a  10051  dfac8clem  10115  dfac5lem4  10209  pwsdompw  10285  cfsuc  10339  cflim2  10345  enfin2i  10403  isf34lem4  10459  axdc4lem  10537  zornn0g  10587  uniimadomf  10633  fpwwe2lem7  10726  fpwwe2lem11  10730  fpwwe2lem12  10731  pwfseqlem1  10747  pwfseqlem5  10752  intgru  10903  addclpi  10981  addnidpi  10990  ltsonq  11058  nqpr  11103  reclem3pr  11138  recexsr  11196  supsrlem  11200  nnnn0addcl  12640  un0addcl  12643  un0mulcl  12644  nn0nndivcl  12682  nn0ge0div  12772  uzind3  12797  uzind4  13037  zsupss  13068  rpnnen1lem2  13109  rpnnen1lem1  13110  rpnnen1lem3  13111  rpnnen1lem5  13113  ltsubrp  13162  ltaddrp  13163  xrlttr  13273  qbtwnxr  13334  xltnegi  13350  xaddnemnf  13370  xaddnepnf  13371  xaddcom  13374  xnegdi  13382  xsubge0  13395  xrub  13446  fzne1  13742  fzind2  13927  seqof  14206  expp1  14215  expneg  14216  expcllem  14219  mulexpz  14249  expaddz  14253  expmulz  14255  faclbnd4lem3  14443  faclbnd4  14445  fi1uzind  14656  swrd00  14797  swrd0  14813  cats1un  14875  reuccatpfxs1  14901  cshw0  14950  cshwn  14953  wwlktovfo  15117  shftf  15238  sqrtdiv  15438  leabs  15472  mulcn2  15769  summolem2  15888  fsumrev2  15954  geomulcvg  16051  prodmolem2  16108  zprod  16110  prodsn  16135  prodsnf  16137  fprodle  16169  bpolydiflem  16226  bpoly2  16229  bpoly3  16230  ruclem6  16409  dvdsflip  16493  dvdsfac  16502  gcdcllem1  16675  lcmgcdlem  16787  rpexp1i  16905  hashdvds  16958  hashgcdlem  16971  phisum  16974  iserodd  17019  pcqcl  17040  pcid  17057  ismred  17778  funcpropd  18083  natpropd  18160  odupos  18506  lubun  18695  rabsubmgmd  18899  sgrpidmnd  18934  issubmd  19007  grpinvnzcl  19227  mulgneg  19308  mulgnn0z  19317  symgfixf1  19657  symgsssg  19687  symgfisg  19688  pgpssslw  19834  sylow2alem2  19838  sylow2a  19839  oddvdssubg  20075  gsumzunsnd  20176  gsumunsnfd  20177  gsum2dlem1  20190  gsum2dlem2  20191  gsumcom3  20198  ablfac1eu  20295  pgpfac1lem5  20301  gsumdixp  20554  dvdsrcl2  20602  01eq0ring  20787  isdrng3lem1  21011  isdrng3lem2  21012  isdrngd  21028  isdrngdOLD  21030  unichnlidl  21522  isprmidlc  21634  ssdifidllem  21646  ssdifidlprm  21648  cnsubrg  21739  psgnodpm  21900  evlslem4  22391  psdmul  22493  coe1tmmul2  22601  mpomatmul  22767  matunitlindflem1  23000  cpmidpmat  23197  intcld  23364  neiptopnei  23456  ordtrest2lem  23527  lmss  23622  cmpcovf  23715  cncmp  23716  fincmp  23717  cmpsublem  23723  cmpsub  23724  unconn  23753  1stcfb  23769  2ndcsep  23784  refun0  23840  locfincmp  23851  1stckgenlem  23878  ptbasin  23902  ptbasfi  23906  ptunimpt  23920  ptuniconst  23923  dfac14  23943  ptcnp  23947  xkoptsub  23979  xkococnlem  23984  xkoinjcn  24012  qtopcmplem  24032  qtophmeo  24142  fbfinnfr  24166  isufil2  24233  isfcls  24334  xmetrtri  24680  xmetrtri2  24681  blssioo  25120  divcn  25195  bndth  25285  clmvscom  25417  resscdrg  25685  minveclem3  25756  finiunmbl  25871  opnmbllem  25928  ismbf2d  25967  itg2seq  26069  bddiblnc  26168  ellimc2  26203  limcmpt2  26210  limcres  26212  dvlem  26222  dvidlem  26241  dvrec  26281  dveflem  26305  dvlip  26319  coe1mul3  26423  dvtaylp  26703  leibpilem2  27275  leibpi  27276  wilthlem2  27402  basellem3  27416  dchreq  27591  dchrsum  27602  lgsval3  27648  lgsdir2lem4  27661  2sqlem6  27756  rpvmasumlem  27820  dchrisum0fno1  27844  rpvmasum2  27845  pntrsumbnd2  27900  ostthlem1  27960  infdesc  27973  nosupno  28066  negbdaylem  28448  expsp1  28821  colmid  29166  plngrotlem2  29272  lmiisolem  29307  dfcgra2  29344  prlngmolem2  29437  axcontlem2  29549  axcontlem7  29554  upgrex  29676  umgredg  29722  umgrpredgv  29724  umgredgne  29729  umgredgnlp  29731  usgredgppr  29783  edgssv2  29785  uspgredg2vlem  29810  usgredg2vlem1  29812  upgrres1  29900  nbuhgr2vtx1edgblem  29938  nbusgrf1o0  29956  hashnbusgrnn0  29963  iscplgredg  30004  uhgrvd00  30121  finsumvtxdg2size  30137  wlkepvtx  30245  wlknewwlksn  30482  wwlksnextfun  30493  wwlksnextsurj  30495  elwwlks2ons3im  30549  wwlks2onsym  30555  clwwlkf  30644  fusgreghash2wspv  30942  numclwwlk5lem  30994  grpoidinvlem3  31114  ablo32  31157  ablomuldiv  31160  ablodivdiv  31161  ablodiv32  31163  nvscom  31237  dipassr  31454  htthlem  31525  hsn0elch  31856  shscli  31925  nmopun  32622  branmfn  32713  mdslj1i  32927  mdslj2i  32928  atss  32954  chcv1  32963  dmdbr5ati  33030  snsssng  33158  ifnebib  33193  fnpreimac  33312  fcnvgreu  33314  isoun  33343  fsuppcurry1  33363  fsuppcurry2  33364  prodpr  33464  prodtp  33465  pmtrprfv2  33696  elrgspnsubrunlem2  33856  nsgmgclem  34009  nsgqusf1olem2  34012  ssmxidllem  34045  qsdrng  34068  1arithufdlem3  34125  ordtrest2NEWlem  34601  esumsplit  34732  esumpad2  34735  esumpcvgval  34757  sigaclcu2  34799  ldgenpisyslem1  34843  volmeas  34911  mbfmco2  34944  omsmeas  35002  oddpwdc  35033  eulerpartlemgvv  35055  ballotlemfc0  35172  ballotlemfcc  35173  prodfzo03  35279  circlemethhgt  35319  bnj1109  35464  bnj1294  35494  bnj545  35572  bnj605  35584  bnj594  35589  bnj934  35612  bnj953  35616  bnj1137  35672  bnj1174  35680  bnj1388  35710  vonf1oonfo  35969  subfacp1lem4  36035  erdszelem7  36049  erdszelem8  36050  erdsze2lem2  36056  resconn  36098  cvmsdisj  36122  cvmscld  36125  satf0op  36229  mclsax  36421  climuzcnv  36523  pocnv  36621  cgrid2  36861  btwncom  36872  btwnswapid2  36876  colinearperm1  36920  colinearperm3  36921  colinearperm2  36922  colinearperm4  36923  lineext  36934  colinbtwnle  36976  broutsideof2  36980  outsideofcom  36986  linecom  37008  linerflx2  37009  lineintmo  37015  fwddifn0  37022  hfext  37027  nmulel1  37057  ntruni  37208  clsint2  37210  neibastop1  37240  weiunlem  37344  bj-snsetex  37969  relowlssretop  38380  pibt2  38434  fin2solem  38623  lindsadd  38630  poimirlem4  38636  poimirlem25  38657  poimirlem32  38664  opnmbllem0  38668  mblfinlem3  38671  mbfposadd  38679  itg2addnclem3  38685  ftc1anclem6  38710  ftc1anc  38713  ac6gf  38760  heibor1lem  38837  isdrngo2  38986  unichnidl  39059  isfldidl  39096  cnf1dd  39116  membpartlem19  39940  lkrss2N  40320  elpadd0  40960  ltrnu  41272  tendoex  42126  cdlemm10N  42269  dicfnN  42334  dihmeetlem2N  42450  dihlatat  42488  lcfrlem9  42701  uzindd  43122  sticksstones1  43290  ofun  43383  nn0addcom  43620  nn0mulcom  43624  zmulcomlem  43625  fsuppind  43712  ismrcd1  43803  isnacs3  43815  pellfundglb  43986  jm2.22  44096  jm2.23  44097  isnumbasgrplem1  44197  hbtlem6  44225  rngunsnply  44265  ordsssucim  44498  mnringmulrcld  45320  dvgrat  45390  cvgdvgrat  45391  nznngen  45394  uzmptshftfval  45424  wfac8prim  46086  rnmptlb  46349  rnmptbddlem  46350  rnmptbd2lem  46354  iccshift  46624  iooshift  46628  liminflbuz2  46919  xlimbr  46931  itgperiod  47085  fourierdlem42  47253  fourierdlem68  47278  fourierdlem93  47303  smfpimne2  47944  elprneb  48193  dfatcolem  48419  modmknepk  48532  ichim  48633  ichnfb  48641  prproropf1olem1  48679  prproropf1olem3  48681  gpgnbgrvtx0  49266  gpgnbgrvtx1  49267  2zlidl  49431  lspsslco  49643  isthincd2  50666  fullthinc  50679