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

Theorem 3imtr4i 280
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 206 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 223 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:  hbxfrbi  1742  nfnt  1767  sbimi  1873  ralimi2  2933  reximi2  2993  r19.28v  3053  r19.29r  3055  r19.30  3063  elex  3185  rmoan  3373  rmoimi2  3376  sseq2  3590  rabss2  3648  undif4  3987  r19.2zb  4013  ralf0OLD  4031  difprsnss  4270  snsspw  4315  uniin  4393  iuniin  4467  iuneq1  4470  iuneq2  4473  iunpwss  4551  eunex  4785  rmorabex  4855  exss  4858  pwunss  4943  soeq2  4979  elopaelxp  5114  reliin  5163  coeq1  5201  coeq2  5202  cnveq  5218  dmeq  5246  dmin  5254  dmcoss  5306  rncoeq  5310  dminss  5466  imainss  5467  dfco2a  5552  iotaex  5785  fundif  5849  fununi  5878  fof  6028  f1ocnv  6062  foco2  6287  isocnv  6480  isotr  6486  oprabid  6576  resiexg  6994  zfrep6  7027  ovmptss  7145  dmtpos  7251  tposfn  7268  smores  7336  omopthlem1  7622  eqer  7664  eqerOLD  7665  ixpeq2  7808  enssdom  7866  fiprc  7924  sbthlem9  7963  infensuc  8023  fipwuni  8215  zfregOLD  8385  zfreg2OLD  8386  dfom3  8427  r1elss  8552  scott0  8632  fin56  9098  dominf  9150  ac6n  9190  brdom4  9233  dominfac  9274  inawina  9391  eltsk2g  9452  ltsosr  9794  ssxr  9986  recgt0ii  10808  sup2  10858  dfnn2  10910  peano2uz2  11341  eluzp1p1  11589  peano2uz  11617  zq  11670  ubmelfzo  12400  expclzlem  12746  wrdeq  13182  wwlktovf  13547  fsum2dlem  14343  fprod2dlem  14549  sin02gt0  14761  divalglem6  14959  qredeu  15210  isfunc  16347  xpcbas  16641  drsdirfi  16761  clatl  16939  tsrss  17046  gimcnv  17532  gsum2dlem1  18192  gsum2dlem2  18193  lmimcnv  18888  xrge0subm  19606  fctop  20618  cctop  20620  alexsubALTlem4  21664  lpbl  22118  xrge0gsumle  22444  xrge0tsms  22445  iirev  22536  iihalf1  22538  iihalf2  22540  iimulcl  22544  vitalilem1  23182  vitalilem1OLD  23183  ply1idom  23688  aacjcl  23886  aannenlem2  23888  ang180lem4  24342  lgslem3  24824  axlowdim  25641  axcontlem2  25645  usgraexmplef  25929  nmobndseqi  27018  axhcompl-zf  27239  hhcmpl  27441  shunssi  27611  spansni  27800  pjoml3i  27829  cmcmlem  27834  nonbooli  27894  lnopco0i  28247  pjnmopi  28391  pjnormssi  28411  hatomistici  28605  cvexchi  28612  cmdmdi  28660  mddmdin0i  28674  cdj3lem3b  28683  disjin  28781  disjin2  28782  xrge0tsmsd  29116  issgon  29513  sxbrsigalem0  29660  eulerpartlemgs2  29769  ballotlem2  29877  ballotth  29926  bnj945  30098  bnj556  30224  bnj557  30225  bnj607  30240  bnj864  30246  bnj969  30270  bnj999  30281  bnj1398  30356  elpotr  30930  dfon2lem8  30939  sltval2  31053  txpss3v  31155  meran1  31580  arg-ax  31585  bj-nfalt  31889  bj-eunex  31987  poimirlem25  32604  poimirlem30  32609  bndss  32755  fldcrng  32973  flddmn  33027  prter1  33182  mzpclall  36308  setindtrs  36610  dgraalem  36734  ifpimim  36873  inintabss  36903  refimssco  36932  cotrintab  36940  intimass  36965  psshepw  37102  nzin  37539  axc11next  37629  iotaexeu  37641  hbexgVD  38164  reuan  39829  aovpcov0  39919  aov0ov0  39922  enege  40096  onego  40097  gboagbo  40178  n0rex  40310  elfzlmr  40366  cusgrop  40660  rusgrpropedg  40784  wwlksn0  41059  mhmismgmhm  41596  sgrpplusgaopALT  41621  rhmisrnghm  41710  srhmsubclem1  41865  srhmsubcALTVlem1  41884  rhmsubcALTVlem3  41899  eluz2cnn0n1  42095  regt1loggt0  42128  rege1logbrege0  42150  rege1logbzge0  42151  relogbmulbexp  42153
  Copyright terms: Public domain W3C validator