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  1045  nic-ax  1747  19.30  1958  19.33b  1962  hbntOLD  2293  necon1bd  2951  pssdifn0  4088  ssdisjOLD  4172  ralnralall  4225  disjss3  4804  somo  5222  frminex  5247  sofld  5740  ordelord  5907  unizlim  6006  f0rn0  6252  funopfv  6398  mpteqb  6463  fvrnressn  6593  funfvima  6657  fpropnf1  6689  fliftfun  6727  weniso  6769  tfinds  7226  tfindsg  7227  tfindes  7229  tfinds2  7230  findsg  7260  frxp  7457  suppssr  7497  rdgsucmptnf  7696  frsucmptn  7705  tz7.49  7711  om00  7827  oewordi  7843  iiner  7989  eroveu  8012  undom  8216  sdomdif  8276  php3  8314  sucdom2  8324  unxpdomlem3  8334  fisseneq  8339  pssnn  8346  ordunifi  8378  isfinite2  8386  fiint  8405  infssuni  8425  ixpfi2  8432  finsschain  8441  ordtypelem10  8600  wofib  8618  wemapsolem  8623  unxpwdom2  8661  inf3lem2  8702  cantnfp1lem3  8753  cantnfp1  8754  setind  8786  r1tr  8815  r1ordg  8817  rankelb  8863  rankxplim3  8920  updjudhf  8968  cardlim  9009  infxpenlem  9047  infxpenc2  9056  dfac5lem4  9160  dfac12k  9182  kmlem13  9197  sornom  9312  fin23lem25  9359  fin23lem21  9374  zorn2lem4  9534  iundom2g  9575  fpwwe2lem12  9676  fpwwe2lem13  9677  pwfseqlem4a  9696  eltsk2g  9786  inttsk  9809  tskord  9815  r1tskina  9817  grudomon  9852  arch  11502  zaddcl  11630  uzm1  11932  xrsupsslem  12351  xrinfmsslem  12352  fsequb  12989  fseqsupubi  12992  ssnn0fi  12999  seqf1o  13057  sq01  13201  ccatalpha  13586  ccat1st1st  13623  swrdccatin1  13704  repsdf2  13746  cshw1  13789  wrdl3s3  13927  rexanre  14306  rexuzre  14312  cau3lem  14314  o1co  14537  rlimcn2  14541  o1of2  14563  lo1add  14577  lo1mul  14578  climcau  14621  climbdd  14622  caucvgb  14630  summo  14668  isumltss  14800  mertenslem2  14837  prodmolem2  14885  prodmo  14886  dvdsaddre2b  15252  bitsfzolem  15379  bitsfzo  15380  bezoutlem4  15482  lcmfeq0b  15566  lcmfunsnlem2  15576  divgcdcoprmex  15603  prmind2  15621  isprm5  15642  prm23ge5  15743  pcqmul  15781  pcadd  15816  prmreclem2  15844  prmreclem5  15847  mul4sq  15881  vdwmc2  15906  ramcl  15956  prmgaplem7  15984  prmlem1a  16036  setsstruct2  16119  divsfval  16430  iscatd2  16564  catpropd  16591  wunfunc  16781  gaorber  17962  psgneu  18147  lsmsubm  18289  pj1eu  18330  efgredlem  18381  qusabl  18489  cygabl  18513  cygctb  18514  lt6abl  18517  gsumval3eu  18526  dprdsubg  18644  ablfac1c  18691  pgpfac1  18700  dvdsrtr  18873  unitgrp  18888  drngmul0or  18991  lvecvs0or  19331  lspdisjb  19349  lspsolvlem  19365  lspprat  19376  lbsextlem2  19382  abvn0b  19525  domnchr  20103  znfld  20132  cygznlem3  20141  obselocv  20295  cpmatacl  20744  chfacfisf  20882  chfacfisfcpmat  20883  0ntr  21098  opnneiid  21153  restntr  21209  hausnei2  21380  nrmsep3  21382  cmpsub  21426  uncmp  21429  dfconn2  21445  cnconn  21448  1stcfb  21471  txuni2  21591  txbas  21593  ptbasin  21603  txcls  21630  txbasval  21632  txlly  21662  txnlly  21663  pthaus  21664  txlm  21674  tx1stc  21676  xkohaus  21679  isufil2  21934  ufileu  21945  cnpflfi  22025  txflf  22032  fclscf  22051  flimfnfcls  22054  alexsubb  22072  alexsubALTlem2  22074  alexsubALTlem4  22076  ptcmplem2  22079  ptcmplem3  22080  cnextcn  22093  qustgplem  22146  prdsmet  22397  blin2  22456  prdsbl  22518  nmolb  22743  tgqioo  22825  reconnlem2  22852  reconn  22853  lebnumlem3  22984  iscau4  23298  cmetcaulem  23307  iscmet3lem2  23311  bcthlem5  23346  minveclem3b  23420  pmltpc  23440  evthicc2  23450  ovolunlem2  23487  ovolicc2lem5  23510  mblsplit  23521  iundisj2  23538  volsup  23545  ioombl1lem4  23550  dyaddisj  23585  dyadmbllem  23588  i1faddlem  23680  itg10a  23697  itg1ge0a  23698  mbfi1flimlem  23709  mbfmullem  23712  itg2add  23746  rolle  23973  dvcvx  24003  itgsubst  24032  tdeglem4  24040  ply1domn  24103  fta1b  24149  plyadd  24193  plymul  24194  coeeu  24201  vieta1  24287  aalioulem6  24312  ulmcaulem  24368  ulmcau  24369  ulmbdd  24372  ulmcn  24373  amgm  24938  mumullem2  25127  ppiublem1  25148  dchrfi  25201  dchrptlem2  25211  dchrptlem3  25212  dchrsum2  25214  lgsdchr  25301  lgsquad2lem2  25331  2sqlem5  25368  2sqb  25378  pntlemp  25520  ostthlem2  25538  ostth  25549  iscgrglt  25630  tgbtwnconn1  25691  colline  25765  lmimid  25907  axcontlem8  26072  axcontlem9  26073  eengtrkg  26086  structgrssvtxlemOLD  26136  numedglnl  26260  uhgr2edg  26321  uspgr2wlkeq  26774  wlkonl1iedg  26793  wlkdlem2  26812  pthdlem2  26896  clwlkclwwlklem2a4  27142  clwwisshclwwsn  27161  clwwlknon1sn  27270  frgr2wwlkeu  27503  frgrreg  27584  frgrregord013  27585  nvmul0or  27836  ubthlem3  28059  axhcompl-zf  28186  hvmul0or  28213  ocnel  28488  pjhthmo  28492  spanuni  28734  spansni  28747  hon0  28983  leopadd  29322  leoptr  29327  mdsymlem6  29598  sumdmdlem2  29609  cdjreui  29622  spc2d  29644  iundisj2f  29732  disjunsn  29736  iundisj2fi  29887  ballotlemimin  30898  bnj23  31115  bnj594  31311  bnj849  31324  txsconn  31552  cvmsdisj  31581  cvmliftlem15  31609  cvmlift2lem10  31623  cvmlift3lem7  31636  mclsppslem  31809  dfon2lem3  32017  dfon2lem5  32019  dfon2lem6  32020  dfon2lem7  32021  dfon2lem8  32022  soseq  32082  frr3g  32107  noprefixmo  32176  noetalem3  32193  ifscgr  32479  cgr3tr4  32487  btwnconn1lem13  32534  seglecgr12  32546  elicc3  32639  neibastop1  32682  tailfb  32700  bj-sngltag  33296  bj-elid  33415  mptsnunlem  33515  finxpreclem6  33563  wl-equsal1i  33661  lindsenlbs  33736  poimirlem26  33767  poimirlem27  33768  ismblfin  33782  itg2addnclem3  33795  ftc1anclem6  33822  fdc  33873  riscer  34119  intidl  34160  ispridlc  34201  prtlem14  34682  prtlem17  34684  lpssat  34822  lssatle  34824  lshpkrlem6  34924  cvrnbtwn  35080  atlatmstc  35128  atlatle  35129  atlrelat1  35130  2at0mat0  35333  trlator0  35980  cdleme0moN  36034  cdlemn11pre  37020  dihord2pre  37035  dihmeetlem20N  37136  dochkrshp4  37199  lcfl6  37310  diophin  37857  diophun  37858  pm10.57  39091  fnchoice  39706  ellimcabssub0  40371  fourierdlem81  40926  fourierdlem93  40938  fzopredsuc  41862  2ffzoeq  41867  iccpartlt  41889  cshword2  41966  prmdvdsfmtnof1lem1  42025  lighneallem4  42056  odd2prm2  42156  even3prm2  42157  sbgoldbst  42195  nnsum4primesevenALTV  42218  nzerooringczr  42601  ply1mulgsumlem1  42703  snlindsntor  42789  islininds2  42802  m1modmmod  42845
  Copyright terms: Public domain W3C validator