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  1194  axc9lem1  1963  equs5  2058  sbiedOLD  2119  rsp2  2831  moi  3279  reu6  3285  sbciegft  3355  elpwunsn  4061  prel12  4196  opthpr  4197  invdisj  4429  reusv1  4640  sotr2  4822  wefrc  4866  tz7.7  4897  ordtr2  4915  relop  5144  elres  5300  iss  5312  funssres  5619  fv3  5870  fmptsnd  6074  funfvima  6126  isomin  6212  sorpsscmpl  6566  peano5  6694  f1oweALT  6758  poxp  6885  soxp  6886  tfr3  7058  tz7.48-1  7098  omordi  7205  odi  7218  omass  7219  oen0  7225  nndi  7262  nnmass  7263  nnmordi  7270  nnmord  7271  eroveu  7396  findcard3  7752  fiint  7786  suplub  7909  hartogs  7958  card2on  7969  unxpwdom2  8003  inf3lem2  8035  epfrs  8151  tcel  8165  dfac2  8500  cfcoflem  8641  infpssr  8677  isf32lem9  8730  axdc3lem4  8822  axcclem  8826  zorn2lem7  8871  ttukeylem6  8883  brdom6disj  8899  ondomon  8927  inar1  9142  gruen  9179  indpi  9274  nqereu  9296  genpn0  9370  distrlem1pr  9392  distrlem5pr  9394  ltexprlem1  9403  reclem4pr  9417  addsrmo  9439  mulsrmo  9440  supsrlem  9477  lelttr  9664  ltletr  9665  ltlen  9675  mulgt1  10390  fzind  10948  eqreznegel  11156  xrlelttr  11348  xrltletr  11349  fzen  11692  elfzodifsumelfzo  11839  bernneq  12247  swrdswrdlem  12634  wrd2ind  12653  reuccats1lem  12655  swrdccatin1  12658  repsdf2  12700  limsupbnd2  13255  rlimuni  13322  mulcn2  13367  rlimno1  13425  ndvdssub  13913  coprmdvds  14091  coprmdvds2  14092  maxprmfct  14102  pceu  14218  infpnlem1  14276  imasaddfnlem  14772  plelttr  15448  gsumval2a  15818  symgfix2  16229  gsmsymgrfixlem1  16240  psgnunilem4  16311  lsmmod  16482  lsmdisj2  16489  efgrelexlemb  16557  pgpfac1lem5  16913  lindfrn  18616  mat1dimcrng  18739  dmatelnd  18758  mdetunilem7  18880  cpmatacl  18977  cpmatmcllem  18979  chfacfisf  19115  chfacfisfcpmat  19116  lmss  19558  lmcnp  19564  hausnei2  19613  isnrm2  19618  isnrm3  19619  cmpsublem  19658  2ndcdisj  19716  1stccnp  19722  txcnpi  19837  txlm  19877  tx1stc  19879  fgss2  20103  fgfil  20104  fgcl  20107  ufileu  20148  rnelfm  20182  fmfnfmlem2  20184  fmfnfmlem4  20186  fmfnfm  20187  ufilcmp  20261  cnpfcf  20270  alexsubALTlem2  20276  alexsubALTlem4  20278  alexsubALT  20279  tmdgsum2  20323  tsmsxp  20385  prdsxmslem2  20760  ivthlem2  21592  ivthlem3  21593  ovolicc2  21661  volfiniun  21685  dyadmax  21735  ellimc3  22011  dvlip2  22124  dvne0  22140  axcontlem4  23939  usgra2edg  24044  usgrares1  24072  nb3graprlem1  24113  iswlkg  24186  usgrcyclnl1  24302  nvnencycllem  24305  3v3e3cycl1  24306  4cycl4v4e  24328  4cycl4dv4e  24330  wwlknred  24385  erclwwlktr  24477  erclwwlkntr  24489  clwlkfoclwwlk  24507  el2wlkonotot0  24534  frg2woteq  24723  numclwwlkovf2ex  24749  frgraregord013  24781  gxnn0add  24938  gxadd  24939  gxnn0mul  24941  gxmul  24942  isch3  25821  ocin  25876  shmodsi  25969  spansneleq  26150  stj  26816  atom1d  26934  atcvat2i  26968  chirredlem1  26971  chirredi  26975  mdsymlem3  26986  mdsymlem6  26989  pconcon  28302  cvmsss2  28345  cvmliftlem7  28362  prodmolem2  28630  dfpo2  28747  dfon2lem9  28786  dfon2  28787  wfr3g  28905  frr3g  28949  frrlem11  28962  cgrextend  29221  btwntriv2  29225  btwncomim  29226  btwnexch3  29233  funtransport  29244  ifscgr  29257  colinearxfr  29288  lineext  29289  fscgr  29293  outsideoftr  29342  itg2addnclem3  29632  itg2addnc  29633  areacirc  29676  trer  29698  finminlem  29700  fnessref  29752  fgmin  29778  ismtybndlem  29892  heibor1lem  29895  prtlem17  30208  pellexlem5  30360  pellex  30362  pell1234qrmulcl  30382  pellfundex  30413  ralxfrd2  31725  usgpredgv  31801  usgpredgvALT  31802  ldepspr  32022  19.41rg  32278  iunconlem2  32690  bnj849  32937  bj-andnotim  33133  bj-alanim  33166  bj-equs5v  33288  riotasvd  33634  lshpsmreu  33781  atnle  33989  cvratlem  34092  cvrat2  34100  3dim1  34138  2llnjN  34238  2lplnj  34291  linepsubN  34423  pmapsub  34439  paddasslem14  34504  pclfinN  34571  ispsubcl2N  34618  pclfinclN  34621  ldilval  34784  trlord  35240  cdlemk36  35584  dihlsscpre  35906  baerlem3lem2  36382  baerlem5alem2  36383  baerlem5blem2  36384
  Copyright terms: Public domain W3C validator