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

Theorem impd 432
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 430 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 32 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  imp32  434  pm3.31  446  syland  483  imp4c  594  imp4d  595  imp5d  602  expimpd  606  expl  622  3expib  1208  axc9lem1  2059  equs5  2149  rsp2  2796  moi  3253  reu6  3259  sbciegft  3330  elpwunsn  4040  prel12  4177  opthpr  4178  invdisj  4412  reusv1  4624  sotr2  4803  wefrc  4847  relop  5004  elres  5159  iss  5171  tz7.7  5468  ordtr2  5486  funssres  5641  fv3  5894  fmptsnd  6101  tpres  6132  funfvima  6155  isomin  6243  sorpsscmpl  6596  peano5  6730  f1oweALT  6791  poxp  6919  soxp  6920  wfr3g  7045  tfr3  7128  tz7.48-1  7171  omordi  7278  odi  7291  omass  7292  oen0  7298  nndi  7335  nnmass  7336  nnmordi  7343  nnmord  7344  eroveu  7469  findcard3  7823  fiint  7857  suplub  7983  hartogs  8068  card2on  8078  unxpwdom2  8112  inf3lem2  8143  epfrs  8223  tcel  8237  dfac2  8568  cfcoflem  8709  infpssr  8745  isf32lem9  8798  axdc3lem4  8890  axcclem  8894  zorn2lem7  8939  ttukeylem6  8951  brdom6disj  8967  ondomon  8995  inar1  9207  gruen  9244  indpi  9339  nqereu  9361  genpn0  9435  distrlem1pr  9457  distrlem5pr  9459  ltexprlem1  9468  reclem4pr  9482  addsrmo  9504  mulsrmo  9505  supsrlem  9542  lelttr  9731  ltletr  9732  ltlen  9742  mulgt1  10471  fzind  11040  eqreznegel  11256  xrlelttr  11460  xrltletr  11461  fzen  11823  elfzodifsumelfzo  11986  bernneq  12404  swrdswrdlem  12817  wrd2ind  12836  reuccats1lem  12838  swrdccatin1  12841  repsdf2  12883  limsupbnd2  13545  limsupbnd2OLD  13546  rlimuni  13613  mulcn2  13658  rlimno1  13716  prodmolem2  13988  ndvdssub  14387  lcmfunsnlem1  14609  lcmfunsnlem2  14612  maxprmfct  14651  coprmdvds  14658  coprmdvds2  14659  pceu  14795  infpnlem1  14853  prmgaplem6  15025  imasaddfnlem  15433  initoeu1  15905  termoeu1  15912  plelttr  16217  gsumval2a  16521  symgfix2  17056  gsmsymgrfixlem1  17067  psgnunilem4  17137  lsmmod  17324  lsmdisj2  17331  efgrelexlemb  17399  pgpfac1lem5  17711  lindfrn  19377  mat1dimcrng  19500  dmatelnd  19519  mdetunilem7  19641  cpmatacl  19738  cpmatmcllem  19740  chfacfisf  19876  chfacfisfcpmat  19877  lmss  20312  lmcnp  20318  hausnei2  20367  isnrm2  20372  isnrm3  20373  cmpsublem  20412  2ndcdisj  20469  1stccnp  20475  txcnpi  20621  txlm  20661  tx1stc  20663  fgss2  20887  fgfil  20888  fgcl  20891  ufileu  20932  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem4  20970  fmfnfm  20971  ufilcmp  21045  cnpfcf  21054  alexsubALTlem2  21061  alexsubALTlem4  21063  alexsubALT  21064  tmdgsum2  21109  tsmsxp  21167  prdsxmslem2  21542  ivthlem2  22401  ivthlem3  22402  ovolicc2  22474  volfiniun  22498  dyadmax  22554  ellimc3  22832  dvlip2  22945  dvne0  22961  axcontlem4  24995  usgra2edg  25107  usgrares1  25136  nb3graprlem1  25177  iswlkg  25250  usgrcyclnl1  25366  nvnencycllem  25369  3v3e3cycl1  25370  4cycl4v4e  25392  4cycl4dv4e  25394  wwlknred  25449  erclwwlktr  25541  erclwwlkntr  25553  clwlkfoclwwlk  25571  el2wlkonotot0  25598  frg2woteq  25786  numclwwlkovf2ex  25812  frgraregord013  25844  gxnn0add  26000  gxadd  26001  gxnn0mul  26003  gxmul  26004  isch3  26892  ocin  26947  shmodsi  27040  spansneleq  27221  stj  27886  atom1d  28004  atcvat2i  28038  chirredlem1  28041  chirredi  28045  mdsymlem3  28056  mdsymlem6  28059  bnj849  29744  pconcon  29962  cvmsss2  30005  cvmliftlem7  30022  mclsind  30216  dfpo2  30402  dfon2lem9  30444  dfon2  30445  frr3g  30520  frrlem11  30533  cgrextend  30780  btwntriv2  30784  btwncomim  30785  btwnexch3  30792  funtransport  30803  ifscgr  30816  colinearxfr  30847  lineext  30848  fscgr  30852  outsideoftr  30901  trer  30977  finminlem  30979  fnessref  31018  fgmin  31031  bj-andnotim  31176  bj-alanim  31203  bj-equs5v  31331  relowlssretop  31730  finxpsuclem  31753  poimirlem29  31933  itg2addnclem3  31959  itg2addnc  31960  areacirc  32001  ismtybndlem  32102  heibor1lem  32105  prtlem17  32416  riotasvd  32497  lshpsmreu  32644  atnle  32852  cvratlem  32955  cvrat2  32963  3dim1  33001  2llnjN  33101  2lplnj  33154  linepsubN  33286  pmapsub  33302  paddasslem14  33367  pclfinN  33434  ispsubcl2N  33481  pclfinclN  33484  ldilval  33647  trlord  34105  cdlemk36  34449  dihlsscpre  34771  baerlem3lem2  35247  baerlem5alem2  35248  baerlem5blem2  35249  pellexlem5  35647  pellex  35649  pell1234qrmulcl  35671  pellfundex  35704  relexpmulnn  36271  19.41rg  36887  iunconlem2  37305  nltle2tri  38586  iccpartnel  38622  bgoldbtbnd  38774  ralxfrd2  38872  funopsn  38881  fundmge2nop  38889  usgrpredgav  39068  usgr2edg  39075  usgredgedga  39091  nbuhgr  39178  nb3grprlem1  39214  usgpredgv  39331  usgpredgvALT  39332  nzerooringczr  39694  ldepspr  39888  aacllem  40162
  Copyright terms: Public domain W3C validator