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

Theorem syl5bir 232
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 217 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 33 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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
This theorem is referenced by:  3imtr3g  283  oplem1  999  nic-ax  1589  19.30  1798  19.33b  1802  hbntOLD  2130  necon1bd  2800  pssdifn0  3898  ssdisjOLD  3979  disjss3  4577  somo  4983  frminex  5008  sofld  5486  ordelord  5648  unizlim  5747  f0rn0  5988  funopfv  6130  mpteqb  6192  fvrnressn  6311  funfvima  6374  fliftfun  6440  weniso  6482  tfinds  6929  tfindsg  6930  tfindes  6932  tfinds2  6933  findsg  6963  frxp  7152  suppssr  7191  rdgsucmptnf  7390  frsucmptn  7399  tz7.49  7405  om00  7520  oewordi  7536  iiner  7684  eroveu  7707  undom  7911  sdomdif  7971  php3  8009  sucdom2  8019  unxpdomlem3  8029  fisseneq  8034  pssnn  8041  ordunifi  8073  isfinite2  8081  fiint  8100  infssuni  8118  ixpfi2  8125  finsschain  8134  ordtypelem10  8293  wofib  8311  wemapsolem  8316  unxpwdom2  8354  inf3lem2  8387  cantnfp1lem3  8438  cantnfp1  8439  setind  8471  r1tr  8500  r1ordg  8502  rankelb  8548  rankxplim3  8605  cardlim  8659  infxpenlem  8697  infxpenc2  8706  dfac5lem4  8810  dfac12k  8830  kmlem13  8845  sornom  8960  fin23lem25  9007  fin23lem21  9022  zorn2lem4  9182  iundom2g  9219  fpwwe2lem12  9320  fpwwe2lem13  9321  pwfseqlem4a  9340  eltsk2g  9430  inttsk  9453  tskord  9459  r1tskina  9461  grudomon  9496  arch  11139  zaddcl  11253  uzm1  11553  xrsupsslem  11968  xrinfmsslem  11969  fsequb  12594  fseqsupubi  12597  ssnn0fi  12604  seqf1o  12662  sq01  12806  ccatalpha  13177  swrdccatin1  13283  repsdf2  13325  cshw1  13368  wrdl3s3  13502  rexanre  13883  rexuzre  13889  cau3lem  13891  o1co  14114  rlimcn2  14118  o1of2  14140  lo1add  14154  lo1mul  14155  climcau  14198  climbdd  14199  caucvgb  14207  summo  14244  isumltss  14368  mertenslem2  14405  prodmolem2  14453  prodmo  14454  dvdsaddre2b  14816  bitsfzolem  14943  bitsfzo  14944  bezoutlem4  15046  lcmfeq0b  15130  lcmfunsnlem2  15140  divgcdcoprmex  15167  prmind2  15185  isprm5  15206  prm23ge5  15307  pcqmul  15345  pcadd  15380  prmreclem2  15408  prmreclem5  15411  mul4sq  15445  vdwmc2  15470  ramcl  15520  prmgaplem7  15548  prmlem1a  15600  divsfval  15979  iscatd2  16114  catpropd  16141  wunfunc  16331  gaorber  17513  psgneu  17698  lsmsubm  17840  pj1eu  17881  efgredlem  17932  qusabl  18040  cygabl  18064  cygctb  18065  lt6abl  18068  gsumval3eu  18077  dprdsubg  18195  ablfac1c  18242  pgpfac1  18251  dvdsrtr  18424  unitgrp  18439  drngmul0or  18540  lvecvs0or  18878  lspdisjb  18896  lspsolvlem  18912  lspprat  18923  lbsextlem2  18929  abvn0b  19072  domnchr  19647  znfld  19676  cygznlem3  19685  obselocv  19839  cpmatacl  20288  chfacfisf  20426  chfacfisfcpmat  20427  0ntr  20633  opnneiid  20688  restntr  20744  hausnei2  20915  nrmsep3  20917  cmpsub  20961  uncmp  20964  dfcon2  20980  cnconn  20983  1stcfb  21006  txuni2  21126  txbas  21128  ptbasin  21138  txcls  21165  txbasval  21167  txlly  21197  txnlly  21198  pthaus  21199  txlm  21209  tx1stc  21211  xkohaus  21214  isufil2  21470  ufileu  21481  cnpflfi  21561  txflf  21568  fclscf  21587  flimfnfcls  21590  alexsubb  21608  alexsubALTlem2  21610  alexsubALTlem4  21612  ptcmplem2  21615  ptcmplem3  21616  cnextcn  21629  qustgplem  21682  prdsmet  21933  blin2  21992  prdsbl  22054  nmolb  22279  tgqioo  22359  reconnlem2  22386  reconn  22387  lebnumlem3  22518  iscau4  22830  cmetcaulem  22839  iscmet3lem2  22843  bcthlem5  22878  minveclem3b  22952  pmltpc  22971  evthicc2  22981  ovolunlem2  23018  ovolicc2lem5  23041  mblsplit  23052  iundisj2  23069  volsup  23076  ioombl1lem4  23081  dyaddisj  23115  dyadmbllem  23118  i1faddlem  23211  itg10a  23228  itg1ge0a  23229  mbfi1flimlem  23240  mbfmullem  23243  itg2add  23277  rolle  23502  dvcvx  23532  itgsubst  23561  tdeglem4  23569  ply1domn  23632  fta1b  23678  plyadd  23722  plymul  23723  coeeu  23730  vieta1  23816  aalioulem6  23841  ulmcaulem  23897  ulmcau  23898  ulmbdd  23901  ulmcn  23902  amgm  24462  mumullem2  24651  ppiublem1  24672  dchrfi  24725  dchrptlem2  24735  dchrptlem3  24736  dchrsum2  24738  lgsdchr  24825  lgsquad2lem2  24855  2sqlem5  24892  2sqb  24902  pntlemp  25044  ostthlem2  25062  ostth  25073  iscgrglt  25155  tgbtwnconn1  25216  colline  25290  lmimid  25432  axcontlem8  25597  axcontlem9  25598  eengtrkg  25611  usgra2edg  25705  usg2wlkeq  26030  clwlkisclwwlklem2a4  26106  clwwisshclwwn  26130  frgraregord013  26439  nvmul0or  26683  ubthlem3  26906  axhcompl-zf  27033  hvmul0or  27060  ocnel  27335  pjhthmo  27339  spanuni  27581  spansni  27594  hon0  27830  leopadd  28169  leoptr  28174  mdsymlem6  28445  sumdmdlem2  28456  cdjreui  28469  spc2d  28491  iundisj2f  28579  disjunsn  28583  iundisj2fi  28737  ballotlemimin  29688  bnj23  29832  bnj594  30030  bnj849  30043  txscon  30271  cvmsdisj  30300  cvmliftlem15  30328  cvmlift2lem10  30342  cvmlift3lem7  30355  mclsppslem  30528  dfon2lem3  30728  dfon2lem5  30730  dfon2lem6  30731  dfon2lem7  30732  dfon2lem8  30733  soseq  30789  frr3g  30817  nodenselem4  30877  nodenselem5  30878  nobndup  30893  nobnddown  30894  ifscgr  31115  cgr3tr4  31123  btwnconn1lem13  31170  seglecgr12  31182  elicc3  31275  neibastop1  31318  tailfb  31336  bj-sngltag  31958  bj-elid  32056  mptsnunlem  32155  finxpreclem6  32203  wl-equsal1i  32302  lindsenlbs  32368  poimirlem26  32399  poimirlem27  32400  ismblfin  32414  itg2addnclem3  32427  ftc1anclem6  32454  fdc  32505  riscer  32751  intidl  32792  ispridlc  32833  prtlem14  32971  prtlem17  32973  lpssat  33112  lssatle  33114  lshpkrlem6  33214  cvrnbtwn  33370  atlatmstc  33418  atlatle  33419  atlrelat1  33420  2at0mat0  33623  trlator0  34270  cdleme0moN  34324  cdlemn11pre  35311  dihord2pre  35326  dihmeetlem20N  35427  dochkrshp4  35490  lcfl6  35601  diophin  36148  diophun  36149  pm10.57  37386  fnchoice  38005  ellimcabssub0  38478  fourierdlem81  38874  fourierdlem93  38886  fzopredsuc  39741  iccpartlt  39757  prmdvdsfmtnof1lem1  39829  lighneallem4  39860  bgoldbst  39995  nnsum4primesevenALTV  40012  cshword2  40095  ralnralall  40102  fpropnf1  40154  2ffzoeq  40178  structgrssvtxlem  40248  uhgr2edg  40427  uspgr2wlkeq  40846  wlkOnl1iedg  40865  1wlkdlem2  40884  pthdlem2  40966  clwlkclwwlklem2a4  41198  clwwisshclwwsn  41228  av-frgrareg  41540  av-frgraregord013  41541  nzerooringczr  41856  ply1mulgsumlem1  41960  snlindsntor  42046  islininds2  42059  m1modmmod  42102
  Copyright terms: Public domain W3C validator