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

Theorem syl5bir 234
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 219 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr3g  286  oplem1  1079  nic-ax  1768  19.30  1980  19.33b  1984  necon1bd  2955  pssdifn0  4110  ralnralall  4239  disjss3  4810  somo  5234  frminex  5259  sofld  5766  ordelord  5932  unizlim  6026  f0rn0  6274  funopfv  6425  mpteqb  6490  fvrnressn  6622  funfvima  6687  fpropnf1  6718  fliftfun  6756  weniso  6798  tfinds  7259  tfindsg  7260  tfindes  7262  tfinds2  7263  findsg  7293  frxp  7491  suppssr  7531  rdgsucmptnf  7731  frsucmptn  7740  tz7.49  7746  om00  7862  oewordi  7878  iiner  8024  eroveu  8048  undom  8257  sdomdif  8317  php3  8355  sucdom2  8365  unxpdomlem3  8375  fisseneq  8380  pssnn  8387  ordunifi  8419  isfinite2  8427  fiint  8446  infssuni  8466  ixpfi2  8473  finsschain  8482  ordtypelem10  8641  wofib  8659  wemapsolem  8664  unxpwdom2  8702  inf3lem2  8743  cantnfp1lem3  8794  cantnfp1  8795  setind  8827  r1tr  8856  r1ordg  8858  rankelb  8904  rankxplim3  8961  updjudhf  9010  cardlim  9051  infxpenlem  9089  infxpenc2  9098  dfac5lem4  9202  dfac12k  9224  kmlem13  9239  sornom  9354  fin23lem25  9401  fin23lem21  9416  zorn2lem4  9576  iundom2g  9617  fpwwe2lem12  9718  fpwwe2lem13  9719  pwfseqlem4a  9738  eltsk2g  9828  inttsk  9851  tskord  9857  r1tskina  9859  grudomon  9894  arch  11537  zaddcl  11667  uzm1  11921  xrsupsslem  12342  xrinfmsslem  12343  fsequb  12985  fseqsupubi  12988  ssnn0fi  12995  seqf1o  13052  sq01  13196  ccatalpha  13567  ccat1st1st  13605  swrdccatin1  13732  repsdf2  13805  cshw1  13854  wrdl3s3  13995  rexanre  14374  rexuzre  14380  cau3lem  14382  o1co  14605  rlimcn2  14609  o1of2  14631  lo1add  14645  lo1mul  14646  climcau  14689  climbdd  14690  caucvgb  14698  summo  14736  isumltss  14867  mertenslem2  14903  prodmolem2  14951  prodmo  14952  dvdsaddre2b  15317  bitsfzolem  15440  bitsfzo  15441  bezoutlem4  15543  lcmfeq0b  15627  lcmfunsnlem2  15637  divgcdcoprmex  15663  prmind2  15681  isprm5  15701  prm23ge5  15802  pcqmul  15840  pcadd  15875  prmreclem2  15903  prmreclem5  15906  mul4sq  15940  vdwmc2  15965  ramcl  16015  prmgaplem7  16043  prmlem1a  16090  setsstruct2  16172  divsfval  16476  iscatd2  16610  catpropd  16637  wunfunc  16827  gaorber  18007  psgneu  18193  lsmsubm  18335  pj1eu  18376  efgredlem  18428  efgredlemOLD  18429  qusabl  18537  cygabl  18561  cygctb  18562  lt6abl  18565  gsumval3eu  18574  dprdsubg  18693  ablfac1c  18740  pgpfac1  18749  dvdsrtr  18922  unitgrp  18937  drngmul0or  19040  lvecvs0or  19383  lspdisjb  19401  lspsolvlem  19418  lspprat  19430  lbsextlem2  19436  abvn0b  19579  domnchr  20156  znfld  20184  cygznlem3  20193  obselocv  20351  cpmatacl  20803  chfacfisf  20941  chfacfisfcpmat  20942  0ntr  21158  opnneiid  21213  restntr  21269  hausnei2  21440  nrmsep3  21442  cmpsub  21486  uncmp  21489  dfconn2  21505  cnconn  21508  1stcfb  21531  txuni2  21651  txbas  21653  ptbasin  21663  txcls  21690  txbasval  21692  txlly  21722  txnlly  21723  pthaus  21724  txlm  21734  tx1stc  21736  xkohaus  21739  isufil2  21994  ufileu  22005  cnpflfi  22085  txflf  22092  fclscf  22111  flimfnfcls  22114  alexsubb  22132  alexsubALTlem2  22134  alexsubALTlem4  22136  ptcmplem2  22139  ptcmplem3  22140  cnextcn  22153  qustgplem  22206  prdsmet  22457  blin2  22516  prdsbl  22578  nmolb  22803  tgqioo  22885  reconnlem2  22912  reconn  22913  lebnumlem3  23044  iscau4  23359  cmetcaulem  23368  iscmet3lem2  23372  bcthlem5  23408  minveclem3b  23491  pmltpc  23511  evthicc2  23521  ovolunlem2  23559  ovolicc2lem5  23582  mblsplit  23593  iundisj2  23610  volsup  23617  ioombl1lem4  23622  dyaddisj  23657  dyadmbllem  23660  i1faddlem  23754  itg10a  23771  itg1ge0a  23772  mbfi1flimlem  23783  mbfmullem  23786  itg2add  23820  rolle  24047  dvcvx  24077  itgsubst  24106  tdeglem4  24114  ply1domn  24177  fta1b  24223  plyadd  24267  plymul  24268  coeeu  24275  vieta1  24361  aalioulem6  24386  ulmcaulem  24442  ulmcau  24443  ulmbdd  24446  ulmcn  24447  amgm  25011  mumullem2  25200  ppiublem1  25221  dchrfi  25274  dchrptlem2  25284  dchrptlem3  25285  dchrsum2  25287  lgsdchr  25374  lgsquad2lem2  25404  2sqlem5  25441  2sqb  25451  pntlemp  25593  ostthlem2  25611  ostth  25622  iscgrglt  25703  tgbtwnconn1  25764  colline  25838  lmimid  25980  axcontlem8  26145  axcontlem9  26146  eengtrkg  26159  numedglnl  26320  uhgr2edg  26381  uspgr2wlkeq  26836  wlkonl1iedg  26855  wlkdlem2  26875  pthdlem2  26959  clwlkclwwlklem2a4  27227  clwwisshclwwsn  27255  clwwlknon1sn  27376  frgr2wwlkeu  27610  frgrreg  27713  frgrregord013  27714  nvmul0or  27964  ubthlem3  28187  axhcompl-zf  28314  hvmul0or  28341  ocnel  28616  pjhthmo  28620  spanuni  28862  spansni  28875  hon0  29111  leopadd  29450  leoptr  29455  mdsymlem6  29726  sumdmdlem2  29737  cdjreui  29750  spc2d  29772  iundisj2f  29854  disjunsn  29858  iundisj2fi  30008  ballotlemimin  31018  bnj23  31238  bnj594  31433  bnj849  31446  txsconn  31674  cvmsdisj  31703  cvmliftlem15  31731  cvmlift2lem10  31745  cvmlift3lem7  31758  mclsppslem  31931  dfon2lem3  32136  dfon2lem5  32138  dfon2lem6  32139  dfon2lem7  32140  dfon2lem8  32141  soseq  32201  frr3g  32226  noprefixmo  32295  noetalem3  32312  ifscgr  32598  cgr3tr4  32606  btwnconn1lem13  32653  seglecgr12  32665  elicc3  32758  neibastop1  32800  tailfb  32818  bj-sngltag  33401  bj-elid  33521  mptsnunlem  33622  finxpreclem6  33669  wl-equsal1i  33757  lindsenlbs  33831  poimirlem26  33862  poimirlem27  33863  ismblfin  33877  itg2addnclem3  33889  ftc1anclem6  33916  fdc  33966  riscer  34212  intidl  34253  ispridlc  34294  prtlem14  34833  prtlem17  34835  lpssat  34972  lssatle  34974  lshpkrlem6  35074  cvrnbtwn  35230  atlatmstc  35278  atlatle  35279  atlrelat1  35280  2at0mat0  35484  trlator0  36130  cdleme0moN  36184  cdlemn11pre  37169  dihord2pre  37184  dihmeetlem20N  37285  dochkrshp4  37348  lcfl6  37459  diophin  38017  diophun  38018  pm10.57  39247  fnchoice  39843  ellimcabssub0  40490  fourierdlem81  41044  fourierdlem93  41056  fzopredsuc  42070  2ffzoeq  42075  iccpartlt  42097  prmdvdsfmtnof1lem1  42175  lighneallem4  42206  odd2prm2  42306  even3prm2  42307  sbgoldbst  42345  nnsum4primesevenALTV  42368  nzerooringczr  42744  ply1mulgsumlem1  42846  snlindsntor  42932  islininds2  42945  m1modmmod  42988
  Copyright terms: Public domain W3C validator