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

Theorem 3imtr4i 279
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3imtr4.1 (𝜑𝜓)
3imtr4.2 (𝜒𝜑)
3imtr4.3 (𝜃𝜓)
Assertion
Ref Expression
3imtr4i (𝜒𝜃)

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3 (𝜒𝜑)
2 3imtr4.1 . . 3 (𝜑𝜓)
31, 2sylbi 205 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 222 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  hbxfrbi  1741  nfnt  1766  sbimi  1872  ralimi2  2932  reximi2  2992  r19.28v  3052  r19.29r  3054  r19.30  3062  elex  3184  rmoan  3372  rmoimi2  3375  sseq2  3589  rabss2  3647  undif4  3986  r19.2zb  4012  ralf0OLD  4030  difprsnss  4269  snsspw  4310  uniin  4387  iuniin  4461  iuneq1  4464  iuneq2  4467  iunpwss  4545  eunex  4780  rmorabex  4849  exss  4852  pwunss  4933  soeq2  4969  elopaelxp  5104  reliin  5152  coeq1  5189  coeq2  5190  cnveq  5206  dmeq  5233  dmin  5241  dmcoss  5293  rncoeq  5297  dminss  5452  imainss  5453  dfco2a  5538  iotaex  5771  fundif  5835  fununi  5864  fof  6013  f1ocnv  6047  foco2  6272  isocnv  6458  isotr  6464  oprabid  6554  resiexg  6971  zfrep6  7004  ovmptss  7122  dmtpos  7228  tposfn  7245  smores  7313  omopthlem1  7599  eqer  7641  eqerOLD  7642  ixpeq2  7785  enssdom  7843  fiprc  7901  sbthlem9  7940  infensuc  8000  fipwuni  8192  zfregOLD  8362  zfreg2OLD  8363  dfom3  8404  r1elss  8529  scott0  8609  fin56  9075  dominf  9127  ac6n  9167  brdom4  9210  dominfac  9251  inawina  9368  eltsk2g  9429  ltsosr  9771  ssxr  9958  recgt0ii  10778  sup2  10828  dfnn2  10880  peano2uz2  11297  eluzp1p1  11545  peano2uz  11573  zq  11626  ubmelfzo  12355  expclzlem  12701  wrdeq  13128  wwlktovf  13493  fsum2dlem  14289  fprod2dlem  14495  sin02gt0  14707  divalglem6  14905  qredeu  15156  isfunc  16293  xpcbas  16587  drsdirfi  16707  clatl  16885  tsrss  16992  gimcnv  17478  gsum2dlem1  18138  gsum2dlem2  18139  lmimcnv  18834  xrge0subm  19552  fctop  20560  cctop  20562  alexsubALTlem4  21606  lpbl  22059  xrge0gsumle  22376  xrge0tsms  22377  iirev  22467  iihalf1  22469  iihalf2  22471  iimulcl  22475  vitalilem1  23099  vitalilem1OLD  23100  ply1idom  23605  aacjcl  23803  aannenlem2  23805  ang180lem4  24259  lgslem3  24741  axlowdim  25559  axcontlem2  25563  usgraexmplef  25695  nmobndseqi  26824  axhcompl-zf  27045  hhcmpl  27247  shunssi  27417  spansni  27606  pjoml3i  27635  cmcmlem  27640  nonbooli  27700  lnopco0i  28053  pjnmopi  28197  pjnormssi  28217  hatomistici  28411  cvexchi  28418  cmdmdi  28466  mddmdin0i  28480  cdj3lem3b  28489  disjin  28587  disjin2  28588  xrge0tsmsd  28922  issgon  29319  sxbrsigalem0  29466  eulerpartlemgs2  29575  ballotlem2  29683  ballotth  29732  bnj945  29904  bnj556  30030  bnj557  30031  bnj607  30046  bnj864  30052  bnj969  30076  bnj999  30087  bnj1398  30162  elpotr  30736  dfon2lem8  30745  sltval2  30859  txpss3v  30961  meran1  31386  arg-ax  31391  bj-nfalt  31695  bj-eunex  31793  poimirlem25  32400  poimirlem30  32405  bndss  32551  fldcrng  32769  flddmn  32823  prter1  32978  mzpclall  36104  setindtrs  36406  dgraalem  36530  ifpimim  36669  inintabss  36699  refimssco  36728  cotrintab  36736  intimass  36761  psshepw  36898  nzin  37335  axc11next  37425  iotaexeu  37437  hbexgVD  37960  reuan  39626  aovpcov0  39717  aov0ov0  39720  enege  39894  onego  39895  gboagbo  39976  n0rex  40108  elfzlmr  40186  cusgrop  40655  rusgrpropedg  40779  wwlksn0  41054  mhmismgmhm  41591  sgrpplusgaopALT  41616  rhmisrnghm  41705  srhmsubclem1  41860  srhmsubcALTVlem1  41879  rhmsubcALTVlem3  41894  eluz2cnn0n1  42090  regt1loggt0  42123  rege1logbrege0  42145  rege1logbzge0  42146  relogbmulbexp  42148
  Copyright terms: Public domain W3C validator