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

Theorem impd 437
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 84 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 435 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 32 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  imp32  439  pm3.31  451  syland  488  imp4c  600  imp4d  601  imp5d  608  expimpd  612  expl  628  3expib  1213  axc9lem1  2094  equs5  2183  rsp2  2761  moi  3189  reu6  3195  sbciegft  3266  elpwunsn  3980  prel12  4121  opthpr  4122  invdisj  4363  reusv1  4576  sotr2  4762  wefrc  4806  relop  4963  elres  5118  iss  5130  tz7.7  5428  ordtr2  5446  funssres  5601  fv3  5861  fmptsnd  6071  tpres  6102  funfvima  6126  isomin  6214  sorpsscmpl  6570  peano5  6704  f1oweALT  6765  poxp  6896  soxp  6897  wfr3g  7021  tfr3  7104  tz7.48-1  7147  omordi  7254  odi  7267  omass  7268  oen0  7274  nndi  7311  nnmass  7312  nnmordi  7319  nnmord  7320  eroveu  7445  findcard3  7801  fiint  7835  suplub  7961  hartogs  8046  card2on  8056  unxpwdom2  8090  inf3lem2  8121  epfrs  8202  tcel  8216  dfac2  8548  cfcoflem  8689  infpssr  8725  isf32lem9  8778  axdc3lem4  8870  axcclem  8874  zorn2lem7  8919  ttukeylem6  8931  brdom6disj  8947  ondomon  8975  inar1  9187  gruen  9224  indpi  9319  nqereu  9341  genpn0  9415  distrlem1pr  9437  distrlem5pr  9439  ltexprlem1  9448  reclem4pr  9462  addsrmo  9484  mulsrmo  9485  supsrlem  9522  lelttr  9711  ltletr  9712  ltlen  9722  mulgt1  10453  fzind  11023  eqreznegel  11239  xrlelttr  11443  xrltletr  11444  fzen  11807  elfzodifsumelfzo  11973  bernneq  12392  swrdswrdlem  12814  wrd2ind  12833  reuccats1lem  12835  swrdccatin1  12838  repsdf2  12880  limsupbnd2  13557  limsupbnd2OLD  13558  rlimuni  13625  mulcn2  13670  rlimno1  13728  prodmolem2  14000  ndvdssub  14399  lcmfunsnlem1  14621  lcmfunsnlem2  14624  maxprmfct  14663  coprmdvds  14670  coprmdvds2  14671  pceu  14807  infpnlem1  14865  prmgaplem6  15037  imasaddfnlem  15445  initoeu1  15917  termoeu1  15924  plelttr  16229  gsumval2a  16533  symgfix2  17068  gsmsymgrfixlem1  17079  psgnunilem4  17149  lsmmod  17336  lsmdisj2  17343  efgrelexlemb  17411  pgpfac1lem5  17723  lindfrn  19390  mat1dimcrng  19513  dmatelnd  19532  mdetunilem7  19654  cpmatacl  19751  cpmatmcllem  19753  chfacfisf  19889  chfacfisfcpmat  19890  lmss  20325  lmcnp  20331  hausnei2  20380  isnrm2  20385  isnrm3  20386  cmpsublem  20425  2ndcdisj  20482  1stccnp  20488  txcnpi  20634  txlm  20674  tx1stc  20676  fgss2  20900  fgfil  20901  fgcl  20904  ufileu  20945  rnelfm  20979  fmfnfmlem2  20981  fmfnfmlem4  20983  fmfnfm  20984  ufilcmp  21058  cnpfcf  21067  alexsubALTlem2  21074  alexsubALTlem4  21076  alexsubALT  21077  tmdgsum2  21122  tsmsxp  21180  prdsxmslem2  21555  ivthlem2  22414  ivthlem3  22415  ovolicc2  22487  volfiniun  22512  dyadmax  22568  ellimc3  22846  dvlip2  22959  dvne0  22975  axcontlem4  25009  usgra2edg  25121  usgrares1  25150  nb3graprlem1  25191  iswlkg  25264  usgrcyclnl1  25380  nvnencycllem  25383  3v3e3cycl1  25384  4cycl4v4e  25406  4cycl4dv4e  25408  wwlknred  25463  erclwwlktr  25555  erclwwlkntr  25567  clwlkfoclwwlk  25585  el2wlkonotot0  25612  frg2woteq  25800  numclwwlkovf2ex  25826  frgraregord013  25858  gxnn0add  26014  gxadd  26015  gxnn0mul  26017  gxmul  26018  isch3  26906  ocin  26961  shmodsi  27054  spansneleq  27235  stj  27900  atom1d  28018  atcvat2i  28052  chirredlem1  28055  chirredi  28059  mdsymlem3  28070  mdsymlem6  28073  bnj849  29742  pconcon  29960  cvmsss2  30003  cvmliftlem7  30020  mclsind  30214  dfpo2  30401  dfon2lem9  30443  dfon2  30444  frr3g  30519  frrlem11  30532  cgrextend  30781  btwntriv2  30785  btwncomim  30786  btwnexch3  30793  funtransport  30804  ifscgr  30817  colinearxfr  30848  lineext  30849  fscgr  30853  outsideoftr  30902  trer  30978  finminlem  30980  fnessref  31019  fgmin  31032  bj-andnotim  31174  bj-alanim  31206  bj-equs5v  31366  relowlssretop  31768  finxpsuclem  31791  poimirlem29  31971  itg2addnclem3  31997  itg2addnc  31998  areacirc  32039  ismtybndlem  32140  heibor1lem  32143  prtlem17  32450  riotasvd  32530  lshpsmreu  32677  atnle  32885  cvratlem  32988  cvrat2  32996  3dim1  33034  2llnjN  33134  2lplnj  33187  linepsubN  33319  pmapsub  33335  paddasslem14  33400  pclfinN  33467  ispsubcl2N  33514  pclfinclN  33517  ldilval  33680  trlord  34138  cdlemk36  34482  dihlsscpre  34804  baerlem3lem2  35280  baerlem5alem2  35281  baerlem5blem2  35282  pellexlem5  35679  pellex  35681  pell1234qrmulcl  35703  pellfundex  35736  relexpmulnn  36303  19.41rg  36918  iunconlem2  37329  nltle2tri  38807  iccpartnel  38843  bgoldbtbnd  38995  ralxfrd2  39100  funopsn  39112  fundmge2nop  39120  xnn0xaddcl  39184  uhgr2edg  39391  ushgredgedga  39408  ushgredgedgaloop  39410  nbuhgr  39513  nb3grprlem1  39556  rusgr1vtx  39705  upgr1wlkwlk  39752  umgrislfupgrlem  39770  uhgr1wlkspthlem2  39838  usgr2wlkneq  39840  cyclnsPth  39874  uspgrn2crct  39878  usgpredgv  40036  usgpredgvALT  40037  nzerooringczr  40399  ldepspr  40591  aacllem  40865
  Copyright terms: Public domain W3C validator