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

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

Proof of Theorem imp31
StepHypRef Expression
1 imp31.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp 407 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 407 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  imp41  426  imp5d  440  impl  456  anassrs  468  an31s  652  3imp  1111  reusv3  5358  otiunsndisj  5475  pwssun  5526  friOLD  5592  ordelord  6337  tz7.7  6341  dfimafn  6902  funimass4  6904  funimass3  7001  isomin  7278  isopolem  7286  onint  7717  limsssuc  7778  tfindsg  7789  findsg  7828  suppfnss  8112  smores2  8292  tfrlem9  8323  tz7.49  8383  oecl  8475  oaordi  8485  oaass  8500  omordi  8505  odi  8518  oen0  8525  nnaordi  8557  nnmordi  8570  php3OLD  9126  domunfican  9222  dfac5  10022  cofsmo  10163  cfcoflem  10166  zorn2lem7  10396  tskwun  10678  mulcanpi  10794  ltexprlem7  10936  sup3  12070  elnnz  12467  nzadd  12509  irradd  12852  irrmul  12853  uzsubsubfz  13417  fzo1fzo0n0  13577  elincfzoext  13584  elfzonelfzo  13628  uzindi  13841  ssnn0fi  13844  sqlecan  14067  swrdnd2  14497  swrdwrdsymb  14504  wrd2ind  14565  repswccat  14628  cshwlen  14641  cshwidxmod  14645  2cshwcshw  14668  wrdl3s3  14805  lcmfunsnlem1  16467  coprmprod  16491  unbenlem  16734  infpnlem1  16736  prmgaplem7  16883  iscatd  17507  dirtr  18445  telgsums  19723  psgndiflemA  20952  isphld  21005  psrbaglefiOLD  21282  gsummoncoe1  21621  gsummatr01lem3  21952  cpmatmcllem  22013  mp2pm2mplem4  22104  chfacfisf  22149  chfacfisfcpmat  22150  cayleyhamilton1  22187  tgcl  22265  neindisj2  22420  2ndcdisj  22753  fgcl  23175  rnelfm  23250  alexsubALTlem3  23346  2sqreultlem  26741  2sqreunnltlem  26744  usgrexmpledg  28055  cusgrsize  28247  uspgr2wlkeqi  28441  usgr2wlkneq  28549  usgr2pthlem  28556  crctcshwlkn0  28611  wwlksnextinj  28689  wwlksnextproplem2  28700  wwlksnextproplem3  28701  clwlkclwwlklem2a  28787  clwlkclwwlklem2  28789  clwwlkf1  28838  clwwlknwwlksnb  28844  clwwlkext2edg  28845  clwwlknonex2lem2  28897  frgr3vlem1  29062  3vfriswmgrlem  29066  vdgn1frgrv2  29085  frgrwopreglem5  29110  frgrwopreglem5ALT  29111  mdexchi  31122  atomli  31169  mdsymlem5  31194  sumdmdlem  31205  dfimafnf  31395  prmidlc  32059  bnj517  33325  bnj1118  33424  mclsind  33992  dfon2lem6  34195  btwnconn1lem11  34614  finminlem  34722  isbasisrelowllem1  35758  isbasisrelowllem2  35759  poimirlem27  36037  itg2addnc  36064  rngoueqz  36331  dmncan1  36467  disjlem19  37195  lshpdisj  37381  2at0mat0  37920  llncvrlpln2  37952  lplncvrlvol2  38010  lhpexle2lem  38404  cdlemk33N  39304  cdlemk34  39305  eldioph2  40988  cantnfresb  41559  gneispacess2  42323  sge0iunmpt  44554  funressnfv  45172  dfaimafn  45292  otiunsndisjX  45406  elfz2z  45442  iccelpart  45520  icceuelpart  45523  fargshiftfva  45530  sprsymrelfo  45584  sbcpr  45608  bgoldbtbndlem4  45895  isomuspgrlem1  45914  isomuspgrlem2b  45916  isomuspgrlem2d  45918  zrtermorngc  46194  zrtermoringc  46263  snlindsntor  46447  ldepspr  46449  nn0sumshdiglemB  46601
  Copyright terms: Public domain W3C validator