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

Theorem 3imtr4i 295
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 220 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 237 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  norassOLD  1535  hbxfrbi  1826  sbimiOLD  2516  sbimiALT  2577  nexmo  2623  moimi  2627  eu6im  2659  ralimi2  3149  reximi2  3232  r19.29rOLD  3244  elisset  3480  elex  3487  rmoan  3705  rmoimi2  3709  reuan  3852  sseq2  3968  rabss2  4029  n0rex  4286  undif4  4388  r19.2zb  4413  difprsnss  4705  snsspw  4748  uniin  4837  iuniin  4906  iuneq1  4910  iuneq2  4913  iunpwss  5004  axrep6  5173  eunex  5268  rmorabex  5329  exss  5332  pwunssOLD  5432  soeq2  5472  elopaelxp  5618  reliin  5667  coeq1  5705  coeq2  5706  cnveq  5721  dmeq  5749  dmin  5757  dmcoss  5820  rncoeq  5824  dminss  5988  imainss  5989  dfco2a  6077  iotaex  6314  fundif  6382  fununi  6408  fof  6572  f1ocnv  6609  foco2  6855  isocnv  7067  isotr  7073  oprabidw  7171  oprabid  7172  zfrep6  7642  ovmptss  7775  dmtpos  7891  tposfn  7908  smores  7976  omopthlem1  8269  eqer  8311  ixpeq2  8462  enssdom  8521  fiprc  8582  sbthlem9  8623  infensuc  8683  fipwuni  8878  dfom3  9098  r1elss  9223  scott0  9303  fin56  9804  dominf  9856  ac6n  9896  brdom4  9941  dominfac  9984  inawina  10101  eltsk2g  10162  ltsosr  10505  ssxr  10699  recgt0ii  11535  sup2  11584  dfnn2  11638  peano2uz2  12058  eluzp1p1  12258  peano2uz  12289  ubmelfzo  13097  elfzlmr  13146  expclzlem  13449  wrdeq  13879  wwlktovf  14311  fsum2dlem  15116  fprod2dlem  15325  sin02gt0  15536  divalglem6  15738  qredeu  15991  isfunc  17125  xpcbas  17419  drsdirfi  17539  clatl  17717  tsrss  17824  smndex1mgm  18063  gimcnv  18398  gsum2dlem1  19081  gsum2dlem2  19082  lmimcnv  19830  xrge0subm  20130  fctop  21607  cctop  21609  alexsubALTlem4  22653  lpbl  23108  xrge0gsumle  23436  xrge0tsms  23437  iirev  23532  iihalf1  23534  iihalf2  23536  iimulcl  23540  vitalilem1  24210  ply1idom  24723  aacjcl  24921  aannenlem2  24923  ang180lem4  25396  lgslem3  25881  tgjustf  26265  axlowdim  26753  axcontlem2  26757  usgrexmplef  27047  cusgrop  27226  rusgrpropedg  27372  spthispth  27513  cycliscrct  27586  wwlksn0  27647  clwwlkccat  27773  clwwlkn  27809  clwwlknonccat  27879  numclwwlk1  28144  nmobndseqi  28560  axhcompl-zf  28779  hhcmpl  28981  shunssi  29149  spansni  29338  pjoml3i  29367  cmcmlem  29372  nonbooli  29432  lnopco0i  29785  pjnmopi  29929  pjnormssi  29949  hatomistici  30143  cvexchi  30150  cmdmdi  30198  mddmdin0i  30212  cdj3lem3b  30221  rmoun  30263  disjin  30344  disjin2  30345  xrge0tsmsd  30723  issgon  31456  sxbrsigalem0  31603  eulerpartlemgs2  31712  ballotlem2  31820  ballotth  31869  bnj945  32119  bnj556  32246  bnj557  32247  bnj607  32262  bnj864  32268  bnj969  32292  bnj999  32304  bnj1398  32380  elpotr  33100  dfon2lem8  33109  sltval2  33237  txpss3v  33413  meran1  33833  arg-ax  33838  bj-nfalt  34119  bj-imdirco  34566  difunieq  34752  pibt1  34794  wl-cbvmotv  34876  poimirlem25  35040  poimirlem30  35045  bndss  35182  fldcrng  35400  flddmn  35454  xrnss3v  35742  redundss3  35981  redundpim3  35983  prter1  36133  mzpclall  39598  setindtrs  39896  dgraalem  40019  ifpimim  40147  inintabss  40208  refimssco  40237  cotrintab  40244  intimass  40285  psshepw  40420  nzin  40956  axc11next  41044  iotaexeu  41056  hbexgVD  41546  absnsb  43558  aovpcov0  43685  aov0ov0  43688  ichan  43911  ichal  43922  spr0el  43938  sprsymrelf  43951  enege  44102  onego  44103  gbogbow  44213  mhmismgmhm  44365  sgrpplusgaopALT  44394  rhmisrnghm  44483  srhmsubclem1  44636  rhmsubcALTVlem3  44669  eluz2cnn0n1  44859  regt1loggt0  44889  rege1logbrege0  44911  rege1logbzge0  44912  relogbmulbexp  44914
  Copyright terms: Public domain W3C validator