MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impd Structured version   Unicode version

Theorem impd 431
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
impd  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem impd
StepHypRef Expression
1 imp3.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3l 81 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 429 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 31 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  imp32  433  pm3.31  445  syland  481  imp4c  591  imp4d  592  imp5d  599  expimpd  603  expl  618  3expib  1200  axc9lem1  1987  equs5  2078  rsp2  2817  moi  3268  reu6  3274  sbciegft  3344  elpwunsn  4055  prel12  4192  opthpr  4193  invdisj  4426  reusv1  4637  sotr2  4819  wefrc  4863  tz7.7  4894  ordtr2  4912  relop  5143  elres  5299  iss  5311  funssres  5618  fv3  5869  fmptsnd  6078  funfvima  6132  isomin  6218  sorpsscmpl  6576  peano5  6708  f1oweALT  6769  poxp  6897  soxp  6898  tfr3  7070  tz7.48-1  7110  omordi  7217  odi  7230  omass  7231  oen0  7237  nndi  7274  nnmass  7275  nnmordi  7282  nnmord  7283  eroveu  7408  findcard3  7765  fiint  7799  suplub  7922  hartogs  7972  card2on  7983  unxpwdom2  8017  inf3lem2  8049  epfrs  8165  tcel  8179  dfac2  8514  cfcoflem  8655  infpssr  8691  isf32lem9  8744  axdc3lem4  8836  axcclem  8840  zorn2lem7  8885  ttukeylem6  8897  brdom6disj  8913  ondomon  8941  inar1  9156  gruen  9193  indpi  9288  nqereu  9310  genpn0  9384  distrlem1pr  9406  distrlem5pr  9408  ltexprlem1  9417  reclem4pr  9431  addsrmo  9453  mulsrmo  9454  supsrlem  9491  lelttr  9678  ltletr  9679  ltlen  9689  mulgt1  10408  fzind  10968  eqreznegel  11177  xrlelttr  11369  xrltletr  11370  fzen  11713  elfzodifsumelfzo  11863  bernneq  12273  swrdswrdlem  12665  wrd2ind  12684  reuccats1lem  12686  swrdccatin1  12689  repsdf2  12731  limsupbnd2  13287  rlimuni  13354  mulcn2  13399  rlimno1  13457  prodmolem2  13723  ndvdssub  14046  coprmdvds  14224  coprmdvds2  14225  maxprmfct  14235  pceu  14351  infpnlem1  14409  imasaddfnlem  14906  plelttr  15580  gsumval2a  15884  symgfix2  16419  gsmsymgrfixlem1  16430  psgnunilem4  16500  lsmmod  16671  lsmdisj2  16678  efgrelexlemb  16746  pgpfac1lem5  17108  lindfrn  18833  mat1dimcrng  18956  dmatelnd  18975  mdetunilem7  19097  cpmatacl  19194  cpmatmcllem  19196  chfacfisf  19332  chfacfisfcpmat  19333  lmss  19776  lmcnp  19782  hausnei2  19831  isnrm2  19836  isnrm3  19837  cmpsublem  19876  2ndcdisj  19934  1stccnp  19940  txcnpi  20086  txlm  20126  tx1stc  20128  fgss2  20352  fgfil  20353  fgcl  20356  ufileu  20397  rnelfm  20431  fmfnfmlem2  20433  fmfnfmlem4  20435  fmfnfm  20436  ufilcmp  20510  cnpfcf  20519  alexsubALTlem2  20525  alexsubALTlem4  20527  alexsubALT  20528  tmdgsum2  20572  tsmsxp  20634  prdsxmslem2  21009  ivthlem2  21841  ivthlem3  21842  ovolicc2  21910  volfiniun  21934  dyadmax  21984  ellimc3  22260  dvlip2  22373  dvne0  22389  axcontlem4  24246  usgra2edg  24358  usgrares1  24386  nb3graprlem1  24427  iswlkg  24500  usgrcyclnl1  24616  nvnencycllem  24619  3v3e3cycl1  24620  4cycl4v4e  24642  4cycl4dv4e  24644  wwlknred  24699  erclwwlktr  24791  erclwwlkntr  24803  clwlkfoclwwlk  24821  el2wlkonotot0  24848  frg2woteq  25036  numclwwlkovf2ex  25062  frgraregord013  25094  gxnn0add  25252  gxadd  25253  gxnn0mul  25255  gxmul  25256  isch3  26135  ocin  26190  shmodsi  26283  spansneleq  26464  stj  27130  atom1d  27248  atcvat2i  27282  chirredlem1  27285  chirredi  27289  mdsymlem3  27300  mdsymlem6  27303  pconcon  28653  cvmsss2  28696  cvmliftlem7  28713  mclsind  28907  dfpo2  29159  dfon2lem9  29198  dfon2  29199  wfr3g  29317  frr3g  29361  frrlem11  29374  cgrextend  29633  btwntriv2  29637  btwncomim  29638  btwnexch3  29645  funtransport  29656  ifscgr  29669  colinearxfr  29700  lineext  29701  fscgr  29705  outsideoftr  29754  itg2addnclem3  30043  itg2addnc  30044  areacirc  30087  trer  30109  finminlem  30111  fnessref  30150  fgmin  30163  ismtybndlem  30277  heibor1lem  30280  prtlem17  30592  pellexlem5  30744  pellex  30746  pell1234qrmulcl  30766  pellfundex  30797  ralxfrd2  32141  usgpredgv  32237  usgpredgvALT  32238  tpres  32390  ldepspr  32809  19.41rg  33056  iunconlem2  33468  bnj849  33716  bj-andnotim  33925  bj-alanim  33952  bj-equs5v  34080  riotasvd  34427  lshpsmreu  34574  atnle  34782  cvratlem  34885  cvrat2  34893  3dim1  34931  2llnjN  35031  2lplnj  35084  linepsubN  35216  pmapsub  35232  paddasslem14  35297  pclfinN  35364  ispsubcl2N  35411  pclfinclN  35414  ldilval  35577  trlord  36035  cdlemk36  36379  dihlsscpre  36701  baerlem3lem2  37177  baerlem5alem2  37178  baerlem5blem2  37179
  Copyright terms: Public domain W3C validator