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  3677  psssstr  4058  reuss2  4272  reupick  4275  reximdva0  4303  falseral0OLD  4471  rabsneu  4690  invdisjrab  5090  opabss  5169  triun  5227  triin  5229  poirr  5575  wefrc  5649  xpcan  6169  fnfco  6740  eqfnun  7029  fnressn  7155  fvtp3  7195  fvtp3g  7198  f1mpt  7258  offval  7687  ordsucuniel  7820  onzsl  7842  soex  7918  fiunlem  7939  fiun  7940  f1iun  7941  dfoprab3  8051  poxp  8126  fnwelem  8129  poxp2  8141  suppssr  8193  suppssrg  8194  suppsssn  8199  suppofssd  8201  fprlem2  8300  oeordsuc  8582  oelim2  8583  omsmolem  8645  ssnnfi  9164  ssfi  9167  ensymfib  9178  domnsymfi  9194  fiint  9296  unifi  9311  indexfi  9327  iinfi  9387  unwdomg  9556  inf3lem5  9611  rankr1bg  9785  rankr1c  9803  carden2a  9971  dfac8clem  10035  dfac5lem4  10129  pwsdompw  10205  cfsuc  10259  cflim2  10265  enfin2i  10323  isf34lem4  10379  axdc4lem  10457  zornn0g  10507  uniimadomf  10553  fpwwe2lem7  10646  fpwwe2lem11  10650  fpwwe2lem12  10651  pwfseqlem1  10667  pwfseqlem5  10672  intgru  10823  addclpi  10901  addnidpi  10910  ltsonq  10978  nqpr  11023  reclem3pr  11058  recexsr  11116  supsrlem  11120  nnnn0addcl  12558  un0addcl  12561  un0mulcl  12562  nn0nndivcl  12600  nn0ge0div  12690  uzind3  12715  uzind4  12955  zsupss  12986  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  ltsubrp  13080  ltaddrp  13081  xrlttr  13191  qbtwnxr  13252  xltnegi  13268  xaddnemnf  13288  xaddnepnf  13289  xaddcom  13292  xnegdi  13300  xsubge0  13313  xrub  13364  fzne1  13659  fzind2  13844  seqof  14123  expp1  14132  expneg  14133  expcllem  14136  mulexpz  14166  expaddz  14170  expmulz  14172  faclbnd4lem3  14359  faclbnd4  14361  fi1uzind  14572  swrd00  14712  swrd0  14728  cats1un  14790  reuccatpfxs1  14816  cshw0  14865  cshwn  14868  wwlktovfo  15031  shftf  15152  sqrtdiv  15352  leabs  15386  mulcn2  15683  summolem2  15802  fsumrev2  15868  geomulcvg  15965  prodmolem2  16022  zprod  16024  prodsn  16049  prodsnf  16051  fprodle  16083  bpolydiflem  16140  bpoly2  16143  bpoly3  16144  ruclem6  16323  dvdsflip  16407  dvdsfac  16416  gcdcllem1  16589  lcmgcdlem  16696  rpexp1i  16814  hashdvds  16866  hashgcdlem  16879  phisum  16882  iserodd  16927  pcqcl  16948  pcid  16965  ismred  17686  funcpropd  17991  natpropd  18068  odupos  18414  lubun  18603  rabsubmgmd  18806  sgrpidmnd  18841  issubmd  18914  grpinvnzcl  19134  mulgneg  19215  mulgnn0z  19224  symgfixf1  19564  symgsssg  19594  symgfisg  19595  pgpssslw  19741  sylow2alem2  19745  sylow2a  19746  oddvdssubg  19982  gsumzunsnd  20083  gsumunsnfd  20084  gsum2dlem1  20097  gsum2dlem2  20098  gsumcom3  20105  ablfac1eu  20202  pgpfac1lem5  20208  gsumdixp  20459  dvdsrcl2  20507  01eq0ring  20691  isdrng3lem1  20914  isdrng3lem2  20915  isdrngd  20931  isdrngdOLD  20933  unichnlidl  21425  isprmidlc  21535  ssdifidllem  21547  ssdifidlprm  21549  cnsubrg  21640  psgnodpm  21801  evlslem4  22292  psdmul  22394  coe1tmmul2  22502  mpomatmul  22668  matunitlindflem1  22901  cpmidpmat  23098  intcld  23265  neiptopnei  23357  ordtrest2lem  23428  lmss  23523  cmpcovf  23616  cncmp  23617  fincmp  23618  cmpsublem  23624  cmpsub  23625  unconn  23654  1stcfb  23670  2ndcsep  23685  refun0  23741  locfincmp  23752  1stckgenlem  23779  ptbasin  23803  ptbasfi  23807  ptunimpt  23821  ptuniconst  23824  dfac14  23844  ptcnp  23848  xkoptsub  23880  xkococnlem  23885  xkoinjcn  23913  qtopcmplem  23933  qtophmeo  24043  fbfinnfr  24067  isufil2  24134  isfcls  24235  xmetrtri  24581  xmetrtri2  24582  blssioo  25021  divcn  25096  bndth  25186  clmvscom  25318  resscdrg  25586  minveclem3  25657  finiunmbl  25772  opnmbllem  25829  ismbf2d  25868  itg2seq  25970  bddiblnc  26069  ellimc2  26104  limcmpt2  26111  limcres  26113  dvlem  26123  dvidlem  26142  dvrec  26182  dveflem  26206  dvlip  26220  coe1mul3  26324  dvtaylp  26606  leibpilem2  27178  leibpi  27179  wilthlem2  27305  basellem3  27319  dchreq  27494  dchrsum  27505  lgsval3  27551  lgsdir2lem4  27564  2sqlem6  27659  rpvmasumlem  27723  dchrisum0fno1  27747  rpvmasum2  27748  pntrsumbnd2  27803  ostthlem1  27863  nosupno  27939  negbdaylem  28321  expsp1  28694  colmid  29039  plngrotlem2  29145  lmiisolem  29180  dfcgra2  29217  prlngmolem2  29310  axcontlem2  29422  axcontlem7  29427  upgrex  29549  umgredg  29595  umgrpredgv  29597  umgredgne  29602  umgredgnlp  29604  usgredgppr  29656  edgssv2  29658  uspgredg2vlem  29683  usgredg2vlem1  29685  upgrres1  29773  nbuhgr2vtx1edgblem  29811  nbusgrf1o0  29829  hashnbusgrnn0  29836  iscplgredg  29877  uhgrvd00  29994  finsumvtxdg2size  30010  wlkepvtx  30118  wlknewwlksn  30355  wwlksnextfun  30366  wwlksnextsurj  30368  elwwlks2ons3im  30422  wwlks2onsym  30428  clwwlkf  30517  fusgreghash2wspv  30815  numclwwlk5lem  30867  grpoidinvlem3  30987  ablo32  31030  ablomuldiv  31033  ablodivdiv  31034  ablodiv32  31036  nvscom  31110  dipassr  31327  htthlem  31398  hsn0elch  31729  shscli  31798  nmopun  32495  branmfn  32586  mdslj1i  32800  mdslj2i  32801  atss  32827  chcv1  32836  dmdbr5ati  32903  snsssng  32989  ifnebib  33024  fnpreimac  33143  fcnvgreu  33145  isoun  33174  fsuppcurry1  33195  fsuppcurry2  33196  prodpr  33296  prodtp  33297  pmtrprfv2  33528  elrgspnsubrunlem2  33688  nsgmgclem  33840  nsgqusf1olem2  33843  ssmxidllem  33876  qsdrng  33899  1arithufdlem3  33956  ordtrest2NEWlem  34432  esumsplit  34563  esumpad2  34566  esumpcvgval  34588  sigaclcu2  34630  ldgenpisyslem1  34674  volmeas  34742  mbfmco2  34776  omsmeas  34834  oddpwdc  34865  eulerpartlemgvv  34887  ballotlemfc0  35004  ballotlemfcc  35005  prodfzo03  35111  circlemethhgt  35151  bnj1109  35296  bnj1294  35326  bnj545  35404  bnj605  35416  bnj594  35421  bnj934  35444  bnj953  35448  bnj1137  35504  bnj1174  35512  bnj1388  35542  vonf1oonfo  35712  subfacp1lem4  35762  erdszelem7  35776  erdszelem8  35777  erdsze2lem2  35783  resconn  35825  cvmsdisj  35849  cvmscld  35852  satf0op  35956  mclsax  36148  climuzcnv  36250  pocnv  36342  cgrid2  36583  btwncom  36594  btwnswapid2  36598  colinearperm1  36642  colinearperm3  36643  colinearperm2  36644  colinearperm4  36645  lineext  36656  colinbtwnle  36698  broutsideof2  36702  outsideofcom  36708  linecom  36730  linerflx2  36731  lineintmo  36737  fwddifn0  36744  hfext  36763  nmulel1  36795  ntruni  36946  clsint2  36948  neibastop1  36978  weiunlem  37082  bj-snsetex  37707  relowlssretop  38117  pibt2  38171  fin2solem  38360  lindsadd  38367  poimirlem4  38373  poimirlem25  38394  poimirlem32  38401  opnmbllem0  38405  mblfinlem3  38408  mbfposadd  38416  itg2addnclem3  38422  ftc1anclem6  38447  ftc1anc  38450  ac6gf  38482  heibor1lem  38559  isdrngo2  38708  unichnidl  38781  isfldidl  38818  cnf1dd  38838  membpartlem19  39662  lkrss2N  40042  elpadd0  40682  ltrnu  40994  tendoex  41848  cdlemm10N  41991  dicfnN  42056  dihmeetlem2N  42172  dihlatat  42210  lcfrlem9  42423  uzindd  42844  sticksstones1  43012  ofun  43105  nn0addcom  43350  nn0mulcom  43354  zmulcomlem  43355  fsuppind  43436  prjspner1  43472  infdesc  43489  ismrcd1  43543  isnacs3  43555  pellfundglb  43726  jm2.22  43836  jm2.23  43837  isnumbasgrplem1  43942  hbtlem6  43970  rngunsnply  44010  ordsssucim  44243  mnringmulrcld  45066  dvgrat  45136  cvgdvgrat  45137  nznngen  45140  uzmptshftfval  45170  wfac8prim  45825  rnmptlb  46072  rnmptbddlem  46073  rnmptbd2lem  46077  iccshift  46348  iooshift  46352  liminflbuz2  46643  xlimbr  46655  itgperiod  46809  fourierdlem42  46977  fourierdlem68  47002  fourierdlem93  47027  smfpimne2  47668  elprneb  47917  dfatcolem  48143  modmknepk  48256  ichim  48357  ichnfb  48365  prproropf1olem1  48403  prproropf1olem3  48405  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  2zlidl  49155  lspsslco  49367  isthincd2  50363  fullthinc  50376