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

Theorem imp31 447
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
impd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp31 (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31
StepHypRef Expression
1 impd.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp 444 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 444 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  imp41  620  imp5d  626  impl  651  anassrs  683  an31s  883  3imp  1102  3impOLD  1103  3expaOLD  1431  reusv3  5025  otiunsndisj  5130  pwssun  5170  fri  5228  predpo  5859  ordelord  5906  tz7.7  5910  dfimafn  6407  funimass4  6409  funimass3  6496  isomin  6750  isopolem  6758  onint  7160  limsssuc  7215  tfindsg  7225  findsg  7258  suppfnss  7488  suppfnssOLD  7489  smores2  7620  tfrlem9  7650  tz7.49  7709  oecl  7786  oaordi  7795  oaass  7810  omordi  7815  odi  7828  oen0  7835  nnaordi  7867  nnmordi  7880  php3  8311  domunfican  8398  dfac5  9141  cofsmo  9283  cfcoflem  9286  zorn2lem7  9516  tskwun  9798  mulcanpi  9914  ltexprlem7  10056  sup3  11172  elnnz  11579  nzadd  11617  irradd  12005  irrmul  12006  uzsubsubfz  12556  fzo1fzo0n0  12713  elincfzoext  12720  elfzonelfzo  12764  uzindi  12975  ssnn0fi  12978  sqlecan  13165  wrd2ind  13677  repswccat  13732  cshwlen  13745  cshwidxmod  13749  2cshwcshw  13771  wrdl3s3  13906  lcmfunsnlem1  15552  lcmfdvdsb  15558  coprmprod  15577  unbenlem  15814  infpnlem1  15816  prmgaplem7  15963  iscatd  16535  initoeu1  16862  termoeu1  16869  dirtr  17437  telgsums  18590  psrbaglefi  19574  gsummoncoe1  19876  psgndiflemA  20149  isphld  20201  gsummatr01lem3  20665  cpmatmcllem  20725  mp2pm2mplem4  20816  chfacfisf  20861  chfacfisfcpmat  20862  cayleyhamilton1  20899  tgcl  20975  neindisj2  21129  2ndcdisj  21461  fgcl  21883  rnelfm  21958  alexsubALTlem3  22054  usgrexmpledg  26353  cusgrsize  26560  uspgr2wlkeqi  26754  usgr2wlkneq  26862  usgr2pthlem  26869  crctcshwlkn0  26924  wwlksnextinj  27017  wwlksnextproplem2  27028  clwlkclwwlklem2a  27121  clwlkclwwlklem2  27123  clwwlkf1  27178  clwwlknwwlksnb  27185  clwwlkext2edg  27186  wwlksext2clwwlk  27187  clwwlknonex2lem2  27257  frgr3vlem1  27427  3vfriswmgrlem  27431  vdgn1frgrv2  27450  frgrwopreglem5  27475  frgrwopreglem5ALT  27476  mdexchi  29503  atomli  29550  mdsymlem5  29575  sumdmdlem  29586  dfimafnf  29745  bnj517  31262  bnj1118  31359  mclsind  31774  dfon2lem6  31998  btwnconn1lem11  32510  finminlem  32618  bj-snmoore  33374  isbasisrelowllem1  33514  isbasisrelowllem2  33515  poimirlem27  33749  itg2addnc  33777  rngoueqz  34052  dmncan1  34188  lshpdisj  34777  2at0mat0  35314  llncvrlpln2  35346  lplncvrlvol2  35404  lhpexle2lem  35798  cdlemk33N  36699  cdlemk34  36700  eldioph2  37827  gneispacess2  38946  sge0iunmpt  41138  funressnfv  41714  dfaimafn  41751  otiunsndisjX  41806  elfz2z  41835  iccelpart  41879  icceuelpart  41882  fargshiftfva  41889  bgoldbtbndlem4  42206  sprsymrelfo  42257  zrtermorngc  42511  zrtermoringc  42580  snlindsntor  42770  ldepspr  42772  nn0sumshdiglemB  42924
  Copyright terms: Public domain W3C validator