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  1006  nic-ax  1595  19.30  1806  19.33b  1810  hbntOLD  2141  necon1bd  2808  pssdifn0  3924  ssdisjOLD  4005  ralnralall  4058  disjss3  4622  somo  5039  frminex  5064  sofld  5550  ordelord  5714  unizlim  5813  f0rn0  6057  funopfv  6202  mpteqb  6265  fvrnressn  6393  funfvima  6457  fpropnf1  6489  fliftfun  6527  weniso  6569  tfinds  7021  tfindsg  7022  tfindes  7024  tfinds2  7025  findsg  7055  frxp  7247  suppssr  7286  rdgsucmptnf  7485  frsucmptn  7494  tz7.49  7500  om00  7615  oewordi  7631  iiner  7779  eroveu  7802  undom  8008  sdomdif  8068  php3  8106  sucdom2  8116  unxpdomlem3  8126  fisseneq  8131  pssnn  8138  ordunifi  8170  isfinite2  8178  fiint  8197  infssuni  8217  ixpfi2  8224  finsschain  8233  ordtypelem10  8392  wofib  8410  wemapsolem  8415  unxpwdom2  8453  inf3lem2  8486  cantnfp1lem3  8537  cantnfp1  8538  setind  8570  r1tr  8599  r1ordg  8601  rankelb  8647  rankxplim3  8704  cardlim  8758  infxpenlem  8796  infxpenc2  8805  dfac5lem4  8909  dfac12k  8929  kmlem13  8944  sornom  9059  fin23lem25  9106  fin23lem21  9121  zorn2lem4  9281  iundom2g  9322  fpwwe2lem12  9423  fpwwe2lem13  9424  pwfseqlem4a  9443  eltsk2g  9533  inttsk  9556  tskord  9562  r1tskina  9564  grudomon  9599  arch  11249  zaddcl  11377  uzm1  11678  xrsupsslem  12096  xrinfmsslem  12097  fsequb  12730  fseqsupubi  12733  ssnn0fi  12740  seqf1o  12798  sq01  12942  ccatalpha  13330  swrdccatin1  13436  repsdf2  13478  cshw1  13521  wrdl3s3  13655  rexanre  14036  rexuzre  14042  cau3lem  14044  o1co  14267  rlimcn2  14271  o1of2  14293  lo1add  14307  lo1mul  14308  climcau  14351  climbdd  14352  caucvgb  14360  summo  14397  isumltss  14524  mertenslem2  14561  prodmolem2  14609  prodmo  14610  dvdsaddre2b  14972  bitsfzolem  15099  bitsfzo  15100  bezoutlem4  15202  lcmfeq0b  15286  lcmfunsnlem2  15296  divgcdcoprmex  15323  prmind2  15341  isprm5  15362  prm23ge5  15463  pcqmul  15501  pcadd  15536  prmreclem2  15564  prmreclem5  15567  mul4sq  15601  vdwmc2  15626  ramcl  15676  prmgaplem7  15704  prmlem1a  15756  setsstruct2  15836  divsfval  16147  iscatd2  16282  catpropd  16309  wunfunc  16499  gaorber  17681  psgneu  17866  lsmsubm  18008  pj1eu  18049  efgredlem  18100  qusabl  18208  cygabl  18232  cygctb  18233  lt6abl  18236  gsumval3eu  18245  dprdsubg  18363  ablfac1c  18410  pgpfac1  18419  dvdsrtr  18592  unitgrp  18607  drngmul0or  18708  lvecvs0or  19048  lspdisjb  19066  lspsolvlem  19082  lspprat  19093  lbsextlem2  19099  abvn0b  19242  domnchr  19820  znfld  19849  cygznlem3  19858  obselocv  20012  cpmatacl  20461  chfacfisf  20599  chfacfisfcpmat  20600  0ntr  20815  opnneiid  20870  restntr  20926  hausnei2  21097  nrmsep3  21099  cmpsub  21143  uncmp  21146  dfconn2  21162  cnconn  21165  1stcfb  21188  txuni2  21308  txbas  21310  ptbasin  21320  txcls  21347  txbasval  21349  txlly  21379  txnlly  21380  pthaus  21381  txlm  21391  tx1stc  21393  xkohaus  21396  isufil2  21652  ufileu  21663  cnpflfi  21743  txflf  21750  fclscf  21769  flimfnfcls  21772  alexsubb  21790  alexsubALTlem2  21792  alexsubALTlem4  21794  ptcmplem2  21797  ptcmplem3  21798  cnextcn  21811  qustgplem  21864  prdsmet  22115  blin2  22174  prdsbl  22236  nmolb  22461  tgqioo  22543  reconnlem2  22570  reconn  22571  lebnumlem3  22702  iscau4  23017  cmetcaulem  23026  iscmet3lem2  23030  bcthlem5  23065  minveclem3b  23139  pmltpc  23159  evthicc2  23169  ovolunlem2  23206  ovolicc2lem5  23229  mblsplit  23240  iundisj2  23257  volsup  23264  ioombl1lem4  23269  dyaddisj  23304  dyadmbllem  23307  i1faddlem  23400  itg10a  23417  itg1ge0a  23418  mbfi1flimlem  23429  mbfmullem  23432  itg2add  23466  rolle  23691  dvcvx  23721  itgsubst  23750  tdeglem4  23758  ply1domn  23821  fta1b  23867  plyadd  23911  plymul  23912  coeeu  23919  vieta1  24005  aalioulem6  24030  ulmcaulem  24086  ulmcau  24087  ulmbdd  24090  ulmcn  24091  amgm  24651  mumullem2  24840  ppiublem1  24861  dchrfi  24914  dchrptlem2  24924  dchrptlem3  24925  dchrsum2  24927  lgsdchr  25014  lgsquad2lem2  25044  2sqlem5  25081  2sqb  25091  pntlemp  25233  ostthlem2  25251  ostth  25262  iscgrglt  25343  tgbtwnconn1  25404  colline  25478  lmimid  25620  axcontlem8  25785  axcontlem9  25786  eengtrkg  25799  structgrssvtxlemOLD  25849  uhgr2edg  26027  uspgr2wlkeq  26445  wlkonl1iedg  26464  wlkdlem2  26483  pthdlem2  26567  clwlkclwwlklem2a4  26799  clwwisshclwwsn  26829  frgrreg  27140  frgrregord013  27141  nvmul0or  27393  ubthlem3  27616  axhcompl-zf  27743  hvmul0or  27770  ocnel  28045  pjhthmo  28049  spanuni  28291  spansni  28304  hon0  28540  leopadd  28879  leoptr  28884  mdsymlem6  29155  sumdmdlem2  29166  cdjreui  29179  spc2d  29201  iundisj2f  29289  disjunsn  29293  iundisj2fi  29439  ballotlemimin  30390  bnj23  30545  bnj594  30743  bnj849  30756  txsconn  30984  cvmsdisj  31013  cvmliftlem15  31041  cvmlift2lem10  31055  cvmlift3lem7  31068  mclsppslem  31241  dfon2lem3  31444  dfon2lem5  31446  dfon2lem6  31447  dfon2lem7  31448  dfon2lem8  31449  soseq  31505  frr3g  31533  nodenselem4  31600  nodenselem5  31601  nobndup  31616  nobnddown  31617  noprefixmo  31626  ifscgr  31846  cgr3tr4  31854  btwnconn1lem13  31901  seglecgr12  31913  elicc3  32006  neibastop1  32049  tailfb  32067  bj-sngltag  32671  bj-elid  32757  mptsnunlem  32856  finxpreclem6  32904  wl-equsal1i  33000  lindsenlbs  33075  poimirlem26  33106  poimirlem27  33107  ismblfin  33121  itg2addnclem3  33134  ftc1anclem6  33161  fdc  33212  riscer  33458  intidl  33499  ispridlc  33540  prtlem14  33678  prtlem17  33680  lpssat  33819  lssatle  33821  lshpkrlem6  33921  cvrnbtwn  34077  atlatmstc  34125  atlatle  34126  atlrelat1  34127  2at0mat0  34330  trlator0  34977  cdleme0moN  35031  cdlemn11pre  36018  dihord2pre  36033  dihmeetlem20N  36134  dochkrshp4  36197  lcfl6  36308  diophin  36855  diophun  36856  pm10.57  38091  fnchoice  38710  ellimcabssub0  39285  fourierdlem81  39741  fourierdlem93  39753  fzopredsuc  40660  2ffzoeq  40665  iccpartlt  40688  cshword2  40766  prmdvdsfmtnof1lem1  40825  lighneallem4  40856  bgoldbst  40991  nnsum4primesevenALTV  41008  nzerooringczr  41390  ply1mulgsumlem1  41492  snlindsntor  41578  islininds2  41591  m1modmmod  41634
  Copyright terms: Public domain W3C validator