Theorem sylan2b 593

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  syl2anb  597  eupickb  2690  2eu1  2705  2eu1v  2707  eqtr3  2818  elnelne1  3100  elnelne2  3101  morex  3646  psssstr  4004  reuss2  4203  reupick  4207  reximdva0  4232  falseral0  4373  rabsneu  4572  opabss  5026  triun  5076  triin  5078  poirr  5373  wefrc  5437  xpcan  5909  fnfco  6411  fnressn  6783  fvtp3  6826  fvtp3g  6829  f1mpt  6884  offval  7274  ordsucuniel  7395  onzsl  7417  soex  7482  fiunlem  7499  fiun  7500  f1iun  7501  dfoprab3  7608  poxp  7675  fnwelem  7678  suppssr  7712  suppsssn  7716  suppofssd  7718  oeordsuc  8070  oelim2  8071  omsmolem  8130  ssnnfi  8583  fiint  8641  unifi  8659  indexfi  8678  iinfi  8727  unwdomg  8894  inf3lem5  8941  rankr1bg  9078  rankr1c  9096  carden2a  9241  dfac8clem  9304  dfac5lem4  9398  pwsdompw  9472  cfsuc  9525  cflim2  9531  enfin2i  9589  isf34lem4  9645  axdc4lem  9723  zornn0g  9773  uniimadomf  9813  fpwwe2lem8  9905  fpwwe2lem12  9909  fpwwe2lem13  9910  pwfseqlem1  9926  pwfseqlem5  9931  intgru  10082  addclpi  10160  addnidpi  10169  ltsonq  10237  nqpr  10282  reclem3pr  10317  recexsr  10375  supsrlem  10379  nnnn0addcl  11775  un0addcl  11778  un0mulcl  11779  nn0nndivcl  11814  nn0ge0div  11900  uzind3  11925  uzind4  12155  zsupss  12186  rpnnen1lem2  12226  rpnnen1lem1  12227  rpnnen1lem3  12228  rpnnen1lem5  12230  ltsubrp  12275  ltaddrp  12276  xrlttr  12383  qbtwnxr  12443  xltnegi  12459  xaddnemnf  12479  xaddnepnf  12480  xaddcom  12483  xnegdi  12491  xsubge0  12504  xrub  12555  fzind2  13005  seqof  13277  expp1  13286  expneg  13287  expcllem  13290  mulexpz  13319  expaddz  13323  expmulz  13325  faclbnd4lem3  13505  faclbnd4  13507  fi1uzind  13701  swrd00  13842  swrd0  13856  cats1un  13919  reuccatpfxs1  13945  cshw0  13992  cshwn  13995  wwlktovfo  14156  shftf  14272  sqrtdiv  14459  leabs  14493  mulcn2  14786  summolem2  14906  fsumrev2  14970  geomulcvg  15065  prodmolem2  15122  zprod  15124  prodsn  15149  prodsnf  15151  fprodle  15183  bpolydiflem  15241  bpoly2  15244  bpoly3  15245  ruclem6  15421  dvdsflip  15500  dvdsfac  15509  gcdcllem1  15681  lcmgcdlem  15779  rpexp1i  15894  hashdvds  15941  hashgcdlem  15954  phisum  15956  iserodd  16001  pcqcl  16022  pcid  16038  ismred  16702  funcpropd  16999  natpropd  17075  lubun  17562  odupos  17574  issubmd  17788  grpinvnzcl  17928  mulgneg  18001  mulgnn0z  18008  symgfixf1  18296  symgsssg  18326  symgfisg  18327  pgpssslw  18469  sylow2alem2  18473  sylow2a  18474  oddvdssubg  18698  gsumzunsnd  18796  gsumunsnfd  18797  gsum2dlem1  18810  gsum2dlem2  18811  ablfac1eu  18912  pgpfac1lem5  18918  gsumdixp  19049  dvdsrcl2  19090  isdrngd  19217  evlslem4  19975  coe1tmmul2  20127  cnsubrg  20287  psgnodpm  20414  gsumcom3  20692  mpomatmul  20739  cpmidpmat  21165  intcld  21332  neiptopnei  21424  ordtrest2lem  21495  lmss  21590  cmpcovf  21683  cncmp  21684  fincmp  21685  cmpsublem  21691  cmpsub  21692  unconn  21721  1stcfb  21737  2ndcsep  21751  refun0  21807  locfincmp  21818  1stckgenlem  21845  ptbasin  21869  ptbasfi  21873  ptunimpt  21887  ptuniconst  21890  dfac14  21910  ptcnp  21914  xkoptsub  21946  xkococnlem  21951  xkoinjcn  21979  qtopcmplem  21999  qtophmeo  22109  fbfinnfr  22133  isufil2  22200  isfcls  22301  xmetrtri  22648  xmetrtri2  22649  blssioo  23086  divcn  23159  bndth  23245  clmvscom  23377  resscdrg  23644  minveclem3  23715  finiunmbl  23828  opnmbllem  23885  ismbf2d  23924  itg2seq  24026  ellimc2  24158  limcmpt2  24165  limcres  24167  dvlem  24177  dvidlem  24196  dvrec  24235  dveflem  24259  dvlip  24273  coe1mul3  24376  dvtaylp  24641  leibpilem2  25201  leibpi  25202  wilthlem2  25328  basellem3  25342  dchreq  25516  dchrsum  25527  lgsval3  25573  lgsdir2lem4  25586  2sqlem6  25681  rpvmasumlem  25745  dchrisum0fno1  25769  rpvmasum2  25770  pntrsumbnd2  25825  ostthlem1  25885  colmid  26156  lmiisolem  26264  dfcgra2  26298  axcontlem2  26434  axcontlem7  26439  upgrex  26560  umgredg  26606  umgrpredgv  26608  umgredgne  26613  umgredgnlp  26615  usgredgppr  26661  edgssv2  26663  uspgredg2vlem  26688  usgredg2vlem1  26690  upgrres1  26778  nbuhgr2vtx1edgblem  26816  nbusgrf1o0  26834  hashnbusgrnn0  26841  iscplgredg  26882  uhgrvd00  26999  finsumvtxdg2size  27015  wlkepvtx  27124  wlknewwlksn  27352  wwlksnextfun  27363  wwlksnextsurj  27365  elwwlks2ons3im  27420  wwlks2onsym  27424  clwwlkf  27513  fusgreghash2wspv  27806  numclwwlk5lem  27858  grpoidinvlem3  27974  ablo32  28017  ablomuldiv  28020  ablodivdiv  28021  ablodiv32  28023  nvscom  28097  dipassr  28314  htthlem  28385  hsn0elch  28716  shscli  28785  nmopun  29482  branmfn  29573  mdslj1i  29787  mdslj2i  29788  atss  29814  chcv1  29823  dmdbr5ati  29890  fnpreimac  30106  fcnvgreu  30108  isoun  30125  fsuppcurry1  30149  fsuppcurry2  30150  prodpr  30226  prodtp  30227  pmtrprfv2  30391  ordtrest2NEWlem  30782  esumsplit  30929  esumpad2  30932  esumpcvgval  30954  sigaclcu2  30996  ldgenpisyslem1  31039  volmeas  31107  mbfmco2  31140  omsmeas  31198  oddpwdc  31229  eulerpartlemgvv  31251  ballotlemfc0  31367  ballotlemfcc  31368  prodfzo03  31491  circlemethhgt  31531  bnj521  31624  bnj1109  31675  bnj1294  31706  bnj545  31783  bnj605  31795  bnj594  31800  bnj934  31823  bnj953  31827  bnj1137  31881  bnj1174  31889  bnj1388  31919  subfacp1lem4  32038  erdszelem7  32052  erdszelem8  32053  erdsze2lem2  32059  resconn  32101  cvmsdisj  32125  cvmscld  32128  satf0op  32232  mclsax  32424  climuzcnv  32522  pocnv  32607  trpredmintr  32679  fprlem2  32747  nosupno  32812  cgrid2  33073  btwncom  33084  btwnswapid2  33088  colinearperm1  33132  colinearperm3  33133  colinearperm2  33134  colinearperm4  33135  lineext  33146  colinbtwnle  33188  broutsideof2  33192  outsideofcom  33198  linecom  33220  linerflx2  33221  lineintmo  33227  fwddifn0  33234  hfext  33253  ntruni  33284  clsint2  33286  neibastop1  33316  bj-snsetex  33880  relowlssretop  34175  pibt2  34229  fin2solem  34409  lindsadd  34416  matunitlindflem1  34419  poimirlem4  34427  poimirlem25  34448  poimirlem32  34455  opnmbllem0  34459  mblfinlem3  34462  mbfposadd  34470  itg2addnclem3  34476  bddiblnc  34493  ftc1anclem6  34503  ftc1anc  34506  eqfnun  34529  ac6gf  34539  heibor1lem  34619  isdrngo2  34768  unichnidl  34841  isfldidl  34878  cnf1dd  34900  lkrss2N  35836  elpadd0  36476  ltrnu  36788  tendoex  37642  cdlemm10N  37785  dicfnN  37850  dihmeetlem2N  37966  dihlatat  38004  lcfrlem9  38217  ismrcd1  38780  isnacs3  38792  pellfundglb  38967  jm2.22  39077  jm2.23  39078  isnumbasgrplem1  39186  hbtlem6  39214  rngunsnply  39258  dvgrat  40182  cvgdvgrat  40183  nznngen  40186  uzmptshftfval  40216  rnmptlb  41055  rnmptbddlem  41056  rnmptbd2lem  41061  iccshift  41336  iooshift  41340  liminflbuz2  41638  xlimbr  41650  itgperiod  41807  fourierdlem42  41976  fourierdlem68  42001  fourierdlem93  42026  elprneb  42780  dfatcolem  42970  ichnfb  43107  prproropf1olem1  43147  prproropf1olem3  43149  rabsubmgmd  43540  2zlidl  43683  lspsslco  43972