Theorem sylan2b 595

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  syl2anb  599  eupickb  2632  2eu1  2647  2eu1v  2648  eqtr3OLD  2760  elnelne1  3058  elnelne2  3059  morex  3716  psssstr  4107  reuss2  4316  reupick  4319  reximdva0  4352  falseral0  4520  rabsneu  4734  invdisjrabw  5134  opabss  5213  triun  5281  triin  5283  poirr  5601  wefrc  5671  xpcan  6176  fnfco  6757  eqfnun  7039  fnressn  7156  fvtp3  7198  fvtp3g  7201  f1mpt  7260  offval  7679  ordsucuniel  7812  onzsl  7835  soex  7912  fiunlem  7928  fiun  7929  f1iun  7930  dfoprab3  8040  poxp  8114  fnwelem  8117  poxp2  8129  suppssr  8181  suppssrg  8182  suppsssn  8186  suppofssd  8188  fprlem2  8286  oeordsuc  8594  oelim2  8595  omsmolem  8656  rexdif1enOLD  9159  ssnnfi  9169  ssnnfiOLD  9170  ssfi  9173  ensymfib  9187  domnsymfi  9203  fiint  9324  unifi  9341  indexfi  9360  iinfi  9412  unwdomg  9579  inf3lem5  9627  rankr1bg  9798  rankr1c  9816  carden2a  9961  dfac8clem  10027  dfac5lem4  10121  pwsdompw  10199  cfsuc  10252  cflim2  10258  enfin2i  10316  isf34lem4  10372  axdc4lem  10450  zornn0g  10500  uniimadomf  10540  fpwwe2lem7  10632  fpwwe2lem11  10636  fpwwe2lem12  10637  pwfseqlem1  10653  pwfseqlem5  10658  intgru  10809  addclpi  10887  addnidpi  10896  ltsonq  10964  nqpr  11009  reclem3pr  11044  recexsr  11102  supsrlem  11106  nnnn0addcl  12502  un0addcl  12505  un0mulcl  12506  nn0nndivcl  12543  nn0ge0div  12631  uzind3  12656  uzind4  12890  zsupss  12921  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  ltsubrp  13010  ltaddrp  13011  xrlttr  13119  qbtwnxr  13179  xltnegi  13195  xaddnemnf  13215  xaddnepnf  13216  xaddcom  13219  xnegdi  13227  xsubge0  13240  xrub  13291  fzind2  13750  seqof  14025  expp1  14034  expneg  14035  expcllem  14038  mulexpz  14068  expaddz  14072  expmulz  14074  faclbnd4lem3  14255  faclbnd4  14257  fi1uzind  14458  swrd00  14594  swrd0  14608  cats1un  14671  reuccatpfxs1  14697  cshw0  14744  cshwn  14747  wwlktovfo  14909  shftf  15026  sqrtdiv  15212  leabs  15246  mulcn2  15540  summolem2  15662  fsumrev2  15728  geomulcvg  15822  prodmolem2  15879  zprod  15881  prodsn  15906  prodsnf  15908  fprodle  15940  bpolydiflem  15998  bpoly2  16001  bpoly3  16002  ruclem6  16178  dvdsflip  16260  dvdsfac  16269  gcdcllem1  16440  lcmgcdlem  16543  rpexp1i  16660  hashdvds  16708  hashgcdlem  16721  phisum  16723  iserodd  16768  pcqcl  16789  pcid  16806  ismred  17546  funcpropd  17851  natpropd  17929  odupos  18281  lubun  18468  sgrpidmnd  18630  issubmd  18687  grpinvnzcl  18895  mulgneg  18972  mulgnn0z  18981  symgfixf1  19305  symgsssg  19335  symgfisg  19336  pgpssslw  19482  sylow2alem2  19486  sylow2a  19487  oddvdssubg  19723  gsumzunsnd  19824  gsumunsnfd  19825  gsum2dlem1  19838  gsum2dlem2  19839  gsumcom3  19846  ablfac1eu  19943  pgpfac1lem5  19949  gsumdixp  20131  dvdsrcl2  20180  01eq0ring  20305  isdrngd  20390  isdrngdOLD  20392  cnsubrg  21005  psgnodpm  21141  evlslem4  21637  coe1tmmul2  21798  mpomatmul  21948  cpmidpmat  22375  intcld  22544  neiptopnei  22636  ordtrest2lem  22707  lmss  22802  cmpcovf  22895  cncmp  22896  fincmp  22897  cmpsublem  22903  cmpsub  22904  unconn  22933  1stcfb  22949  2ndcsep  22963  refun0  23019  locfincmp  23030  1stckgenlem  23057  ptbasin  23081  ptbasfi  23085  ptunimpt  23099  ptuniconst  23102  dfac14  23122  ptcnp  23126  xkoptsub  23158  xkococnlem  23163  xkoinjcn  23191  qtopcmplem  23211  qtophmeo  23321  fbfinnfr  23345  isufil2  23412  isfcls  23513  xmetrtri  23861  xmetrtri2  23862  blssioo  24311  divcn  24384  bndth  24474  clmvscom  24606  resscdrg  24875  minveclem3  24946  finiunmbl  25061  opnmbllem  25118  ismbf2d  25157  itg2seq  25260  bddiblnc  25359  ellimc2  25394  limcmpt2  25401  limcres  25403  dvlem  25413  dvidlem  25432  dvrec  25472  dveflem  25496  dvlip  25510  coe1mul3  25617  dvtaylp  25882  leibpilem2  26446  leibpi  26447  wilthlem2  26573  basellem3  26587  dchreq  26761  dchrsum  26772  lgsval3  26818  lgsdir2lem4  26831  2sqlem6  26926  rpvmasumlem  26990  dchrisum0fno1  27014  rpvmasum2  27015  pntrsumbnd2  27070  ostthlem1  27130  nosupno  27206  negsbdaylem  27530  colmid  27939  lmiisolem  28047  dfcgra2  28081  axcontlem2  28223  axcontlem7  28228  upgrex  28352  umgredg  28398  umgrpredgv  28400  umgredgne  28405  umgredgnlp  28407  usgredgppr  28453  edgssv2  28455  uspgredg2vlem  28480  usgredg2vlem1  28482  upgrres1  28570  nbuhgr2vtx1edgblem  28608  nbusgrf1o0  28626  hashnbusgrnn0  28633  iscplgredg  28674  uhgrvd00  28791  finsumvtxdg2size  28807  wlkepvtx  28917  wlknewwlksn  29141  wwlksnextfun  29152  wwlksnextsurj  29154  elwwlks2ons3im  29208  wwlks2onsym  29212  clwwlkf  29300  fusgreghash2wspv  29588  numclwwlk5lem  29640  grpoidinvlem3  29759  ablo32  29802  ablomuldiv  29805  ablodivdiv  29806  ablodiv32  29808  nvscom  29882  dipassr  30099  htthlem  30170  hsn0elch  30501  shscli  30570  nmopun  31267  branmfn  31358  mdslj1i  31572  mdslj2i  31573  atss  31599  chcv1  31608  dmdbr5ati  31675  snsssng  31752  ifnebib  31781  fnpreimac  31896  fcnvgreu  31898  isoun  31923  fsuppcurry1  31950  fsuppcurry2  31951  fzne1  31999  prodpr  32032  prodtp  32033  pmtrprfv2  32249  nsgmgclem  32522  nsgqusf1olem2  32525  isprmidlc  32566  ssmxidllem  32589  qsdrng  32611  ordtrest2NEWlem  32902  esumsplit  33051  esumpad2  33054  esumpcvgval  33076  sigaclcu2  33118  ldgenpisyslem1  33161  volmeas  33229  mbfmco2  33264  omsmeas  33322  oddpwdc  33353  eulerpartlemgvv  33375  ballotlemfc0  33491  ballotlemfcc  33492  prodfzo03  33615  circlemethhgt  33655  bnj1109  33797  bnj1294  33828  bnj545  33906  bnj605  33918  bnj594  33923  bnj934  33946  bnj953  33950  bnj1137  34006  bnj1174  34014  bnj1388  34044  subfacp1lem4  34174  erdszelem7  34188  erdszelem8  34189  erdsze2lem2  34195  resconn  34237  cvmsdisj  34261  cvmscld  34264  satf0op  34368  mclsax  34560  climuzcnv  34656  pocnv  34733  cgrid2  34975  btwncom  34986  btwnswapid2  34990  colinearperm1  35034  colinearperm3  35035  colinearperm2  35036  colinearperm4  35037  lineext  35048  colinbtwnle  35090  broutsideof2  35094  outsideofcom  35100  linecom  35122  linerflx2  35123  lineintmo  35129  fwddifn0  35136  hfext  35155  gg-divcn  35163  ntruni  35212  clsint2  35214  neibastop1  35244  bj-snsetex  35844  relowlssretop  36244  pibt2  36298  fin2solem  36474  lindsadd  36481  matunitlindflem1  36484  poimirlem4  36492  poimirlem25  36513  poimirlem32  36520  opnmbllem0  36524  mblfinlem3  36527  mbfposadd  36535  itg2addnclem3  36541  ftc1anclem6  36566  ftc1anc  36569  ac6gf  36600  heibor1lem  36677  isdrngo2  36826  unichnidl  36899  isfldidl  36936  cnf1dd  36958  membpartlem19  37681  lkrss2N  38039  elpadd0  38680  ltrnu  38992  tendoex  39846  cdlemm10N  39989  dicfnN  40054  dihmeetlem2N  40170  dihlatat  40208  lcfrlem9  40421  uzindd  40842  sticksstones1  40962  metakunt12  40996  ofun  41058  fsuppind  41162  nn0addcom  41323  nn0mulcom  41327  zmulcomlem  41328  prjspner1  41368  infdesc  41385  ismrcd1  41436  isnacs3  41448  pellfundglb  41623  jm2.22  41734  jm2.23  41735  isnumbasgrplem1  41843  hbtlem6  41871  rngunsnply  41915  ordsssucim  42153  mnringmulrcld  42987  dvgrat  43071  cvgdvgrat  43072  nznngen  43075  uzmptshftfval  43105  rnmptlb  43947  rnmptbddlem  43948  rnmptbd2lem  43952  iccshift  44231  iooshift  44235  liminflbuz2  44531  xlimbr  44543  itgperiod  44697  fourierdlem42  44865  fourierdlem68  44890  fourierdlem93  44915  smfpimne2  45556  elprneb  45739  dfatcolem  45963  ichim  46125  ichnfb  46133  prproropf1olem1  46171  prproropf1olem3  46173  rabsubmgmd  46561  2zlidl  46832  lspsslco  47118  isthincd2  47658  fullthinc  47666