Theorem sylan2b 605

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anb  609  eupickb  2663  2eu1  2678  2eu1v  2679  elnelne1  3075  elnelne2  3076  morex  3683  psssstr  4065  reuss2  4280  reupick  4283  reximdva0  4311  falseral0OLD  4477  rabsneu  4696  invdisjrab  5097  opabss  5176  triun  5234  triin  5236  poirr  5583  wefrc  5657  xpcan  6176  fnfco  6745  eqfnun  7034  fnressn  7157  fvtp3  7197  fvtp3g  7200  f1mpt  7261  offval  7685  ordsucuniel  7821  onzsl  7843  soex  7919  fiunlem  7940  fiun  7941  f1iun  7942  dfoprab3  8052  poxp  8125  fnwelem  8128  poxp2  8140  suppssr  8192  suppssrg  8193  suppsssn  8198  suppofssd  8200  fprlem2  8299  oeordsuc  8581  oelim2  8582  omsmolem  8644  ssnnfi  9155  ssfi  9158  ensymfib  9169  domnsymfi  9185  fiint  9287  unifi  9302  indexfi  9318  iinfi  9378  unwdomg  9547  inf3lem5  9602  rankr1bg  9776  rankr1c  9794  carden2a  9953  dfac8clem  10017  dfac5lem4  10111  pwsdompw  10187  cfsuc  10242  cflim2  10248  enfin2i  10306  isf34lem4  10362  axdc4lem  10440  zornn0g  10490  uniimadomf  10530  fpwwe2lem7  10623  fpwwe2lem11  10627  fpwwe2lem12  10628  pwfseqlem1  10644  pwfseqlem5  10649  intgru  10800  addclpi  10878  addnidpi  10887  ltsonq  10955  nqpr  11000  reclem3pr  11035  recexsr  11093  supsrlem  11097  nnnn0addcl  12535  un0addcl  12538  un0mulcl  12539  nn0nndivcl  12577  nn0ge0div  12666  uzind3  12691  uzind4  12931  zsupss  12962  rpnnen1lem2  13002  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  ltsubrp  13055  ltaddrp  13056  xrlttr  13166  qbtwnxr  13227  xltnegi  13243  xaddnemnf  13263  xaddnepnf  13264  xaddcom  13267  xnegdi  13275  xsubge0  13288  xrub  13339  fzne1  13634  fzind2  13819  seqof  14097  expp1  14106  expneg  14107  expcllem  14110  mulexpz  14140  expaddz  14144  expmulz  14146  faclbnd4lem3  14333  faclbnd4  14335  fi1uzind  14546  swrd00  14684  swrd0  14698  cats1un  14760  reuccatpfxs1  14786  cshw0  14833  cshwn  14836  wwlktovfo  14997  shftf  15118  sqrtdiv  15318  leabs  15352  mulcn2  15649  summolem2  15769  fsumrev2  15835  geomulcvg  15932  prodmolem2  15991  zprod  15993  prodsn  16018  prodsnf  16020  fprodle  16052  bpolydiflem  16109  bpoly2  16112  bpoly3  16113  ruclem6  16292  dvdsflip  16376  dvdsfac  16385  gcdcllem1  16558  lcmgcdlem  16665  rpexp1i  16783  hashdvds  16835  hashgcdlem  16848  phisum  16851  iserodd  16896  pcqcl  16917  pcid  16934  ismred  17655  funcpropd  17960  natpropd  18037  odupos  18383  lubun  18572  rabsubmgmd  18763  sgrpidmnd  18798  issubmd  18865  grpinvnzcl  19078  mulgneg  19159  mulgnn0z  19168  symgfixf1  19508  symgsssg  19538  symgfisg  19539  pgpssslw  19685  sylow2alem2  19689  sylow2a  19690  oddvdssubg  19926  gsumzunsnd  20027  gsumunsnfd  20028  gsum2dlem1  20041  gsum2dlem2  20042  gsumcom3  20049  ablfac1eu  20146  pgpfac1lem5  20152  gsumdixp  20401  dvdsrcl2  20449  01eq0ring  20615  isdrngd  20850  isdrngdOLD  20852  unichnlidl  21343  isprmidlc  21453  ssdifidllem  21465  ssdifidlprm  21467  cnsubrg  21558  psgnodpm  21719  evlslem4  22208  psdmul  22310  coe1tmmul2  22418  mpomatmul  22584  cpmidpmat  23011  intcld  23178  neiptopnei  23270  ordtrest2lem  23341  lmss  23436  cmpcovf  23529  cncmp  23530  fincmp  23531  cmpsublem  23537  cmpsub  23538  unconn  23567  1stcfb  23583  2ndcsep  23597  refun0  23653  locfincmp  23664  1stckgenlem  23691  ptbasin  23715  ptbasfi  23719  ptunimpt  23733  ptuniconst  23736  dfac14  23756  ptcnp  23760  xkoptsub  23792  xkococnlem  23797  xkoinjcn  23825  qtopcmplem  23845  qtophmeo  23955  fbfinnfr  23979  isufil2  24046  isfcls  24147  xmetrtri  24493  xmetrtri2  24494  blssioo  24933  divcn  25008  bndth  25098  clmvscom  25230  resscdrg  25498  minveclem3  25569  finiunmbl  25684  opnmbllem  25741  ismbf2d  25780  itg2seq  25882  bddiblnc  25982  ellimc2  26017  limcmpt2  26024  limcres  26026  dvlem  26036  dvidlem  26055  dvrec  26095  dveflem  26119  dvlip  26133  coe1mul3  26237  dvtaylp  26514  leibpilem2  27087  leibpi  27088  wilthlem2  27214  basellem3  27228  dchreq  27403  dchrsum  27414  lgsval3  27460  lgsdir2lem4  27473  2sqlem6  27568  rpvmasumlem  27632  dchrisum0fno1  27656  rpvmasum2  27657  pntrsumbnd2  27712  ostthlem1  27772  nosupno  27848  negbdaylem  28230  expsp1  28603  colmid  28946  plngrotlem2  29051  lmiisolem  29086  dfcgra2  29122  prlngmolem2  29184  axcontlem2  29296  axcontlem7  29301  upgrex  29423  umgredg  29469  umgrpredgv  29471  umgredgne  29476  umgredgnlp  29478  usgredgppr  29527  edgssv2  29529  uspgredg2vlem  29554  usgredg2vlem1  29556  upgrres1  29644  nbuhgr2vtx1edgblem  29682  nbusgrf1o0  29700  hashnbusgrnn0  29707  iscplgredg  29748  uhgrvd00  29865  finsumvtxdg2size  29881  wlkepvtx  29989  wlknewwlksn  30217  wwlksnextfun  30228  wwlksnextsurj  30230  elwwlks2ons3im  30284  wwlks2onsym  30290  clwwlkf  30379  fusgreghash2wspv  30667  numclwwlk5lem  30719  grpoidinvlem3  30839  ablo32  30882  ablomuldiv  30885  ablodivdiv  30886  ablodiv32  30888  nvscom  30962  dipassr  31179  htthlem  31250  hsn0elch  31581  shscli  31650  nmopun  32347  branmfn  32438  mdslj1i  32652  mdslj2i  32653  atss  32679  chcv1  32688  dmdbr5ati  32755  snsssng  32841  ifnebib  32876  fnpreimac  32996  fcnvgreu  32998  isoun  33028  fsuppcurry1  33050  fsuppcurry2  33051  prodpr  33151  prodtp  33152  pmtrprfv2  33389  elrgspnsubrunlem2  33549  nsgmgclem  33701  nsgqusf1olem2  33704  ssmxidllem  33737  qsdrng  33760  1arithufdlem3  33817  ordtrest2NEWlem  34293  esumsplit  34424  esumpad2  34427  esumpcvgval  34449  sigaclcu2  34491  ldgenpisyslem1  34534  volmeas  34602  mbfmco2  34636  omsmeas  34694  oddpwdc  34725  eulerpartlemgvv  34747  ballotlemfc0  34864  ballotlemfcc  34865  prodfzo03  34971  circlemethhgt  35011  bnj1109  35156  bnj1294  35186  bnj545  35264  bnj605  35276  bnj594  35281  bnj934  35304  bnj953  35308  bnj1137  35364  bnj1174  35372  bnj1388  35402  vonf1oonfo  35580  subfacp1lem4  35656  erdszelem7  35670  erdszelem8  35671  erdsze2lem2  35677  resconn  35719  cvmsdisj  35743  cvmscld  35746  satf0op  35850  mclsax  36042  climuzcnv  36144  pocnv  36236  cgrid2  36476  btwncom  36487  btwnswapid2  36491  colinearperm1  36535  colinearperm3  36536  colinearperm2  36537  colinearperm4  36538  lineext  36549  colinbtwnle  36591  broutsideof2  36595  outsideofcom  36601  linecom  36623  linerflx2  36624  lineintmo  36630  fwddifn0  36637  hfext  36656  nmulel1  36673  ntruni  36819  clsint2  36821  neibastop1  36851  weiunlem  36955  bj-snsetex  37580  relowlssretop  37990  pibt2  38044  fin2solem  38238  lindsadd  38245  matunitlindflem1  38248  poimirlem4  38256  poimirlem25  38277  poimirlem32  38284  opnmbllem0  38288  mblfinlem3  38291  mbfposadd  38299  itg2addnclem3  38305  ftc1anclem6  38330  ftc1anc  38333  ac6gf  38364  heibor1lem  38441  isdrngo2  38590  unichnidl  38663  isfldidl  38700  cnf1dd  38720  membpartlem19  39544  lkrss2N  39924  elpadd0  40564  ltrnu  40876  tendoex  41730  cdlemm10N  41873  dicfnN  41938  dihmeetlem2N  42054  dihlatat  42092  lcfrlem9  42305  uzindd  42726  sticksstones1  42894  ofun  42987  nn0addcom  43217  nn0mulcom  43221  zmulcomlem  43222  fsuppind  43305  prjspner1  43341  infdesc  43358  ismrcd1  43412  isnacs3  43424  pellfundglb  43595  jm2.22  43705  jm2.23  43706  isnumbasgrplem1  43811  hbtlem6  43839  rngunsnply  43879  ordsssucim  44112  mnringmulrcld  44935  dvgrat  45005  cvgdvgrat  45006  nznngen  45009  uzmptshftfval  45039  wfac8prim  45694  rnmptlb  45941  rnmptbddlem  45942  rnmptbd2lem  45946  iccshift  46217  iooshift  46221  liminflbuz2  46512  xlimbr  46524  itgperiod  46678  fourierdlem42  46846  fourierdlem68  46871  fourierdlem93  46896  smfpimne2  47537  elprneb  47749  dfatcolem  47975  modmknepk  48088  ichim  48189  ichnfb  48197  prproropf1olem1  48235  prproropf1olem3  48237  gpgnbgrvtx0  48822  gpgnbgrvtx1  48823  2zlidl  48988  lspsslco  49200  isthincd2  50198  fullthinc  50211