MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bir Structured version   Visualization version   GIF version

Theorem syl5bir 233
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
syl5bir.1 (𝜓𝜑)
syl5bir.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bir (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3 (𝜓𝜑)
21biimpri 218 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr3g  284  oplem1  1027  nic-ax  1638  19.30  1849  19.33b  1853  hbntOLD  2183  necon1bd  2841  pssdifn0  3977  ssdisjOLD  4060  ralnralall  4113  disjss3  4684  somo  5098  frminex  5123  sofld  5616  ordelord  5783  unizlim  5882  f0rn0  6128  funopfv  6273  mpteqb  6338  fvrnressn  6468  funfvima  6532  fpropnf1  6564  fliftfun  6602  weniso  6644  tfinds  7101  tfindsg  7102  tfindes  7104  tfinds2  7105  findsg  7135  frxp  7332  suppssr  7371  rdgsucmptnf  7570  frsucmptn  7579  tz7.49  7585  om00  7700  oewordi  7716  iiner  7862  eroveu  7885  undom  8089  sdomdif  8149  php3  8187  sucdom2  8197  unxpdomlem3  8207  fisseneq  8212  pssnn  8219  ordunifi  8251  isfinite2  8259  fiint  8278  infssuni  8298  ixpfi2  8305  finsschain  8314  ordtypelem10  8473  wofib  8491  wemapsolem  8496  unxpwdom2  8534  inf3lem2  8564  cantnfp1lem3  8615  cantnfp1  8616  setind  8648  r1tr  8677  r1ordg  8679  rankelb  8725  rankxplim3  8782  cardlim  8836  infxpenlem  8874  infxpenc2  8883  dfac5lem4  8987  dfac12k  9007  kmlem13  9022  sornom  9137  fin23lem25  9184  fin23lem21  9199  zorn2lem4  9359  iundom2g  9400  fpwwe2lem12  9501  fpwwe2lem13  9502  pwfseqlem4a  9521  eltsk2g  9611  inttsk  9634  tskord  9640  r1tskina  9642  grudomon  9677  arch  11327  zaddcl  11455  uzm1  11756  xrsupsslem  12175  xrinfmsslem  12176  fsequb  12814  fseqsupubi  12817  ssnn0fi  12824  seqf1o  12882  sq01  13026  ccatalpha  13411  ccat1st1st  13448  swrdccatin1  13529  repsdf2  13571  cshw1  13614  wrdl3s3  13751  rexanre  14130  rexuzre  14136  cau3lem  14138  o1co  14361  rlimcn2  14365  o1of2  14387  lo1add  14401  lo1mul  14402  climcau  14445  climbdd  14446  caucvgb  14454  summo  14492  isumltss  14624  mertenslem2  14661  prodmolem2  14709  prodmo  14710  dvdsaddre2b  15076  bitsfzolem  15203  bitsfzo  15204  bezoutlem4  15306  lcmfeq0b  15390  lcmfunsnlem2  15400  divgcdcoprmex  15427  prmind2  15445  isprm5  15466  prm23ge5  15567  pcqmul  15605  pcadd  15640  prmreclem2  15668  prmreclem5  15671  mul4sq  15705  vdwmc2  15730  ramcl  15780  prmgaplem7  15808  prmlem1a  15860  setsstruct2  15943  divsfval  16254  iscatd2  16389  catpropd  16416  wunfunc  16606  gaorber  17787  psgneu  17972  lsmsubm  18114  pj1eu  18155  efgredlem  18206  qusabl  18314  cygabl  18338  cygctb  18339  lt6abl  18342  gsumval3eu  18351  dprdsubg  18469  ablfac1c  18516  pgpfac1  18525  dvdsrtr  18698  unitgrp  18713  drngmul0or  18816  lvecvs0or  19156  lspdisjb  19174  lspsolvlem  19190  lspprat  19201  lbsextlem2  19207  abvn0b  19350  domnchr  19928  znfld  19957  cygznlem3  19966  obselocv  20120  cpmatacl  20569  chfacfisf  20707  chfacfisfcpmat  20708  0ntr  20923  opnneiid  20978  restntr  21034  hausnei2  21205  nrmsep3  21207  cmpsub  21251  uncmp  21254  dfconn2  21270  cnconn  21273  1stcfb  21296  txuni2  21416  txbas  21418  ptbasin  21428  txcls  21455  txbasval  21457  txlly  21487  txnlly  21488  pthaus  21489  txlm  21499  tx1stc  21501  xkohaus  21504  isufil2  21759  ufileu  21770  cnpflfi  21850  txflf  21857  fclscf  21876  flimfnfcls  21879  alexsubb  21897  alexsubALTlem2  21899  alexsubALTlem4  21901  ptcmplem2  21904  ptcmplem3  21905  cnextcn  21918  qustgplem  21971  prdsmet  22222  blin2  22281  prdsbl  22343  nmolb  22568  tgqioo  22650  reconnlem2  22677  reconn  22678  lebnumlem3  22809  iscau4  23123  cmetcaulem  23132  iscmet3lem2  23136  bcthlem5  23171  minveclem3b  23245  pmltpc  23265  evthicc2  23275  ovolunlem2  23312  ovolicc2lem5  23335  mblsplit  23346  iundisj2  23363  volsup  23370  ioombl1lem4  23375  dyaddisj  23410  dyadmbllem  23413  i1faddlem  23505  itg10a  23522  itg1ge0a  23523  mbfi1flimlem  23534  mbfmullem  23537  itg2add  23571  rolle  23798  dvcvx  23828  itgsubst  23857  tdeglem4  23865  ply1domn  23928  fta1b  23974  plyadd  24018  plymul  24019  coeeu  24026  vieta1  24112  aalioulem6  24137  ulmcaulem  24193  ulmcau  24194  ulmbdd  24197  ulmcn  24198  amgm  24762  mumullem2  24951  ppiublem1  24972  dchrfi  25025  dchrptlem2  25035  dchrptlem3  25036  dchrsum2  25038  lgsdchr  25125  lgsquad2lem2  25155  2sqlem5  25192  2sqb  25202  pntlemp  25344  ostthlem2  25362  ostth  25373  iscgrglt  25454  tgbtwnconn1  25515  colline  25589  lmimid  25731  axcontlem8  25896  axcontlem9  25897  eengtrkg  25910  structgrssvtxlemOLD  25960  numedglnl  26084  uhgr2edg  26145  uspgr2wlkeq  26598  wlkonl1iedg  26617  wlkdlem2  26636  pthdlem2  26720  clwlkclwwlklem2a4  26963  clwwisshclwwsn  26973  clwwlknon1sn  27075  frgr2wwlkeu  27307  frgrreg  27381  frgrregord013  27382  nvmul0or  27633  ubthlem3  27856  axhcompl-zf  27983  hvmul0or  28010  ocnel  28285  pjhthmo  28289  spanuni  28531  spansni  28544  hon0  28780  leopadd  29119  leoptr  29124  mdsymlem6  29395  sumdmdlem2  29406  cdjreui  29419  spc2d  29441  iundisj2f  29529  disjunsn  29533  iundisj2fi  29684  ballotlemimin  30695  bnj23  30912  bnj594  31108  bnj849  31121  txsconn  31349  cvmsdisj  31378  cvmliftlem15  31406  cvmlift2lem10  31420  cvmlift3lem7  31433  mclsppslem  31606  dfon2lem3  31814  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  soseq  31879  frr3g  31904  noprefixmo  31973  noetalem3  31990  ifscgr  32276  cgr3tr4  32284  btwnconn1lem13  32331  seglecgr12  32343  elicc3  32436  neibastop1  32479  tailfb  32497  bj-sngltag  33096  bj-elid  33215  mptsnunlem  33315  finxpreclem6  33363  wl-equsal1i  33459  lindsenlbs  33534  poimirlem26  33565  poimirlem27  33566  ismblfin  33580  itg2addnclem3  33593  ftc1anclem6  33620  fdc  33671  riscer  33917  intidl  33958  ispridlc  33999  prtlem14  34478  prtlem17  34480  lpssat  34618  lssatle  34620  lshpkrlem6  34720  cvrnbtwn  34876  atlatmstc  34924  atlatle  34925  atlrelat1  34926  2at0mat0  35129  trlator0  35776  cdleme0moN  35830  cdlemn11pre  36816  dihord2pre  36831  dihmeetlem20N  36932  dochkrshp4  36995  lcfl6  37106  diophin  37653  diophun  37654  pm10.57  38887  fnchoice  39502  ellimcabssub0  40167  fourierdlem81  40722  fourierdlem93  40734  fzopredsuc  41658  2ffzoeq  41663  iccpartlt  41685  cshword2  41762  prmdvdsfmtnof1lem1  41821  lighneallem4  41852  odd2prm2  41952  even3prm2  41953  sbgoldbst  41991  nnsum4primesevenALTV  42014  nzerooringczr  42397  ply1mulgsumlem1  42499  snlindsntor  42585  islininds2  42598  m1modmmod  42641
  Copyright terms: Public domain W3C validator