Theorem sylan2b 491

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  syl2anb  495  eupickb  2526  eqtr3  2631  elnelne1  2893  elnelne2  2894  morex  3357  psssstr  3675  reuss2  3866  reupick  3870  reximdva0  3891  rabsneu  4208  opabss  4646  triun  4694  poirr  4970  wefrc  5032  xpcan  5489  fnfco  5982  fnressn  6330  fvtp3  6367  fvtp3g  6370  f1mpt  6419  offval  6802  ordsucuniel  6916  onzsl  6938  soex  7002  fun11iun  7019  dfoprab3  7115  1stconst  7152  2ndconst  7153  poxp  7176  fnwelem  7179  suppssr  7213  suppsssn  7217  oeordsuc  7561  oelim2  7562  omsmolem  7620  ssnnfi  8064  fiint  8122  unifi  8138  indexfi  8157  iinfi  8206  unwdomg  8372  inf3lem5  8412  rankr1bg  8549  rankr1c  8567  carden2a  8675  dfac8clem  8738  dfac5lem4  8832  pwsdompw  8909  cfsuc  8962  cflim2  8968  enfin2i  9026  isf34lem4  9082  axdc4lem  9160  zornn0g  9210  uniimadomf  9246  fpwwe2lem8  9338  fpwwe2lem12  9342  fpwwe2lem13  9343  pwfseqlem1  9359  pwfseqlem5  9364  intgru  9515  addclpi  9593  addnidpi  9602  ltsonq  9670  nqpr  9715  reclem3pr  9750  recexsr  9807  supsrlem  9811  nnnn0addcl  11200  un0addcl  11203  un0mulcl  11204  nn0nndivcl  11239  nn0ge0div  11322  uzind3  11347  uzind4  11622  zsupss  11653  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  ltsubrp  11742  ltaddrp  11743  xrlttr  11849  qbtwnxr  11905  xltnegi  11921  xaddnemnf  11941  xaddnepnf  11942  xaddcom  11945  xnegdi  11950  xsubge0  11963  xrub  12014  fzind2  12448  seqof  12720  expp1  12729  expneg  12730  expcllem  12733  mulexpz  12762  expaddz  12766  expmulz  12768  faclbnd4lem3  12944  faclbnd4  12946  fi1uzind  13134  fi1uzindOLD  13140  swrd00  13270  swrd0  13286  cats1un  13327  reuccats1  13332  cshw0  13391  cshwn  13394  wwlktovfo  13549  shftf  13667  sqrtdiv  13854  leabs  13887  mulcn2  14174  summolem2  14294  fsumrev2  14356  geomulcvg  14446  prodmolem2  14504  zprod  14506  prodsn  14531  prodsnf  14533  bpolydiflem  14624  bpoly2  14627  bpoly3  14628  ruclem6  14803  dvdsflip  14877  dvdsfac  14886  gcdcllem1  15059  lcmgcdlem  15157  rpexp1i  15271  hashdvds  15318  hashgcdlem  15331  phisum  15333  iserodd  15378  pcqcl  15399  pcid  15415  ismred  16085  funcpropd  16383  natpropd  16459  lubun  16946  odupos  16958  issubmd  17172  grpinvnzcl  17310  mulgneg  17383  mulgnn0z  17390  symgfixf1  17680  symgsssg  17710  symgfisg  17711  pgpssslw  17852  sylow2alem2  17856  sylow2a  17857  oddvdssubg  18081  gsumzunsnd  18178  gsumunsnfd  18179  gsum2dlem1  18192  gsum2dlem2  18193  ablfac1eu  18295  pgpfac1lem5  18301  gsumdixp  18432  dvdsrcl2  18473  isdrngd  18595  evlslem4  19329  coe1tmmul2  19467  cnsubrg  19625  psgnodpm  19753  gsumcom3  20024  mpt2matmul  20071  cpmidpmat  20497  intcld  20654  neiptopnei  20746  ordtrest2lem  20817  lmss  20912  cmpcovf  21004  cncmp  21005  fincmp  21006  cmpsublem  21012  cmpsub  21013  uncon  21042  1stcfb  21058  2ndcsep  21072  refun0  21128  locfincmp  21139  1stckgenlem  21166  ptbasin  21190  ptbasfi  21194  ptunimpt  21208  ptuniconst  21211  dfac14  21231  ptcnp  21235  xkoptsub  21267  xkococnlem  21272  xkoinjcn  21300  qtopcmplem  21320  qtophmeo  21430  fbfinnfr  21455  isufil2  21522  isfcls  21623  xmetrtri  21970  xmetrtri2  21971  blssioo  22406  divcn  22479  bndth  22565  clmvscom  22698  resscdrg  22962  minveclem3  23008  finiunmbl  23119  opnmbllem  23175  ismbf2d  23214  itg2seq  23315  ellimc2  23447  limcmpt2  23454  limcres  23456  dvlem  23466  dvidlem  23485  dvrec  23524  dveflem  23546  dvlip  23560  coe1mul3  23663  dvtaylp  23928  leibpilem2  24468  leibpi  24469  wilthlem2  24595  basellem3  24609  dchreq  24783  dchrsum  24794  lgsval3  24840  lgsdir2lem4  24853  2sqlem6  24948  rpvmasumlem  24976  dchrisum0fno1  25000  rpvmasum2  25001  pntrsumbnd2  25056  ostthlem1  25116  colmid  25383  lmiisolem  25488  dfcgra2  25521  axcontlem2  25645  axcontlem7  25650  upgrex  25759  umgredg  25812  umgrpredgav  25813  umgredgne  25816  umgredgnlp  25818  umgraex  25852  usgraidx2vlem1  25920  nbgraf1olem3  25972  nbgraf1olem5  25974  cusconngra  26204  wlknwwlknfun  26238  wlknwwlkninj  26239  wlknwwlknsur  26240  wlkiswwlkfun  26245  wlkiswwlkinj  26246  wlkiswwlksur  26247  wwlkextfun  26257  wwlkextsur  26259  wlkv0  26288  clwwlkf  26322  grpoidinvlem3  26744  ablo32  26787  ablomuldiv  26790  ablodivdiv  26791  ablodiv32  26793  nvscom  26868  dipassr  27085  htthlem  27158  hsn0elch  27489  shscli  27560  nmopun  28257  branmfn  28348  mdslj1i  28562  mdslj2i  28563  atss  28589  chcv1  28598  dmdbr5ati  28665  fcnvgreu  28855  isoun  28862  ordtrest2NEWlem  29296  esumsplit  29442  esumpad2  29445  esumpcvgval  29467  sigaclcu2  29510  ldgenpisyslem1  29553  volmeas  29621  mbfmco2  29654  omsmeas  29712  oddpwdc  29743  eulerpartlemgvv  29765  ballotlemfc0  29881  ballotlemfcc  29882  bnj521  30059  bnj1109  30111  bnj1294  30142  bnj545  30219  bnj605  30231  bnj594  30236  bnj934  30259  bnj953  30263  bnj1137  30317  bnj1174  30325  bnj1388  30355  subfacp1lem4  30419  erdszelem7  30433  erdszelem8  30434  erdsze2lem2  30440  rescon  30482  cvmsdisj  30506  cvmscld  30509  mclsax  30720  climuzcnv  30819  pocnv  30907  trpredmintr  30975  cgrid2  31280  btwncom  31291  btwnswapid2  31295  colinearperm1  31339  colinearperm3  31340  colinearperm2  31341  colinearperm4  31342  lineext  31353  colinbtwnle  31395  broutsideof2  31399  outsideofcom  31405  linecom  31427  linerflx2  31428  lineintmo  31434  fwddifn0  31441  hfext  31460  ntruni  31492  clsint2  31494  neibastop1  31524  bj-snsetex  32144  relowlssretop  32387  fin2solem  32565  matunitlindflem1  32575  poimirlem4  32583  poimirlem25  32604  poimirlem32  32611  opnmbllem0  32615  mblfinlem3  32618  mbfposadd  32627  itg2addnclem3  32633  bddiblnc  32650  ftc1anclem6  32660  ftc1anc  32663  eqfnun  32686  ac6gf  32697  heibor1lem  32778  isdrngo2  32927  unichnidl  33000  isfldidl  33037  cnf1dd  33062  lkrss2N  33474  elpadd0  34113  ltrnu  34425  tendoex  35281  cdlemm10N  35425  dicfnN  35490  dihmeetlem2N  35606  dihlatat  35644  lcfrlem9  35857  ismrcd1  36279  isnacs3  36291  pellfundglb  36467  jm2.22  36580  jm2.23  36581  isnumbasgrplem1  36690  hbtlem6  36718  rngunsnply  36762  dvgrat  37533  cvgdvgrat  37534  nznngen  37537  uzmptshftfval  37567  iccshift  38591  iooshift  38595  itgperiod  38873  fourierdlem42  39042  fourierdlem68  39067  fourierdlem93  39092  elprneb  39939  falseral0  40308  usgredgappr  40423  edgassv2  40425  uspgredg2vlem  40450  usgredg2vlem1  40452  upgrres1  40532  nbuhgr2vtx1edgblem  40573  nbusgrf1o0  40597  hashnbusgrnn0  40604  iscplgredg  40639  uhgrvd00  40750  1wlkepvtx  40868  wlknewwlksn  41084  wlknwwlksnfun  41085  wlknwwlksninj  41086  wlknwwlksnsur  41087  wlkwwlkfun  41092  wlkwwlkinj  41093  wlkwwlksur  41094  wwlksnextfun  41104  wwlksnextsur  41106  elwwlks2ons3  41159  clwwlksf  41222  fusgreghash2wspv  41499  rabsubmgmd  41581  2zlidl  41724  lspsslco  42020  setrec2lem2  42240