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  1190  axc9lem1  1945  equs5  2042  sbiedOLD  2103  rsp2  2776  moi  3140  reu6  3146  sbciegft  3215  elpwunsn  3915  prel12  4047  opthpr  4048  invdisj  4279  reusv1  4490  sotr2  4668  wefrc  4712  tz7.7  4743  ordtr2  4761  relop  4988  elres  5143  iss  5152  funssres  5456  fv3  5701  funfvima  5950  isomin  6026  sorpsscmpl  6369  peano5  6497  f1oweALT  6559  poxp  6682  soxp  6683  tfr3  6856  tz7.48-1  6896  omordi  7003  odi  7016  omass  7017  oen0  7023  nndi  7060  nnmass  7061  nnmordi  7068  nnmord  7069  eroveu  7193  findcard3  7553  fiint  7586  suplub  7708  hartogs  7756  card2on  7767  unxpwdom2  7801  inf3lem2  7833  epfrs  7949  tcel  7963  dfac2  8298  cfcoflem  8439  infpssr  8475  isf32lem9  8528  axdc3lem4  8620  axcclem  8624  zorn2lem7  8669  ttukeylem6  8681  brdom6disj  8697  ondomon  8725  inar1  8940  gruen  8977  indpi  9074  nqereu  9096  genpn0  9170  distrlem1pr  9192  distrlem5pr  9194  ltexprlem1  9203  reclem4pr  9217  mulcmpblnr  9239  supsrlem  9276  lelttr  9463  ltletr  9464  ltlen  9474  mulgt1  10186  fzind  10738  eqreznegel  10938  xrlelttr  11128  xrltletr  11129  fzen  11465  elfzodifsumelfzo  11602  bernneq  11988  swrdswrdlem  12351  wrd2ind  12370  swrdccatin1  12372  repsdf2  12414  limsupbnd2  12959  rlimuni  13026  mulcn2  13071  rlimno1  13129  ndvdssub  13609  coprmdvds  13786  coprmdvds2  13787  maxprmfct  13797  pceu  13911  infpnlem1  13969  imasaddfnlem  14464  plelttr  15140  gsumval2a  15510  symgfix2  15919  gsmsymgrfixlem1  15930  psgnunilem4  16001  lsmmod  16170  lsmdisj2  16177  efgrelexlemb  16245  pgpfac1lem5  16578  lindfrn  18248  mdetunilem7  18422  lmss  18900  lmcnp  18906  hausnei2  18955  isnrm2  18960  isnrm3  18961  cmpsublem  19000  2ndcdisj  19058  1stccnp  19064  txcnpi  19179  txlm  19219  tx1stc  19221  fgss2  19445  fgfil  19446  fgcl  19449  ufileu  19490  rnelfm  19524  fmfnfmlem2  19526  fmfnfmlem4  19528  fmfnfm  19529  ufilcmp  19603  cnpfcf  19612  alexsubALTlem2  19618  alexsubALTlem4  19620  alexsubALT  19621  tmdgsum2  19665  tsmsxp  19727  prdsxmslem2  20102  ivthlem2  20934  ivthlem3  20935  ovolicc2  21003  volfiniun  21026  dyadmax  21076  ellimc3  21352  dvlip2  21465  dvne0  21481  axcontlem4  23211  usgra2edg  23299  usgrares1  23321  nb3graprlem1  23357  usgrcyclnl1  23524  nvnencycllem  23527  3v3e3cycl1  23528  4cycl4v4e  23550  4cycl4dv4e  23552  gxnn0add  23759  gxadd  23760  gxnn0mul  23762  gxmul  23763  isch3  24642  ocin  24697  shmodsi  24790  spansneleq  24971  stj  25637  atom1d  25755  atcvat2i  25789  chirredlem1  25792  chirredi  25796  mdsymlem3  25807  mdsymlem6  25810  pconcon  27118  cvmsss2  27161  cvmliftlem7  27178  prodmolem2  27446  dfpo2  27563  dfon2lem9  27602  dfon2  27603  wfr3g  27721  frr3g  27765  frrlem11  27778  cgrextend  28037  btwntriv2  28041  btwncomim  28042  btwnexch3  28049  funtransport  28060  ifscgr  28073  colinearxfr  28104  lineext  28105  fscgr  28109  outsideoftr  28158  itg2addnclem3  28442  itg2addnc  28443  areacirc  28486  trer  28508  finminlem  28510  fnessref  28562  fgmin  28588  ismtybndlem  28702  heibor1lem  28705  prtlem17  29018  pellexlem5  29171  pellex  29173  pell1234qrmulcl  29193  pellfundex  29224  ralxfrd2  30134  iswlkg  30282  wwlknred  30352  el2wlkonotot0  30388  erclwwlktr  30482  erclwwlkntr  30498  clwlkfoclwwlk  30515  frg2woteq  30650  numclwwlkovf2ex  30676  frgraregord013  30708  fmptsnd  30719  telescfzgsum  30807  mat1dimcrng  30870  dmatelnd  30872  pmattomply1f1  30919  ldepspr  31004  19.41rg  31256  iunconlem2  31668  bnj849  31915  bj-andnotim  32111  bj-alanim  32142  bj-equs5v  32264  riotasvd  32604  lshpsmreu  32751  atnle  32959  cvratlem  33062  cvrat2  33070  3dim1  33108  2llnjN  33208  2lplnj  33261  linepsubN  33393  pmapsub  33409  paddasslem14  33474  pclfinN  33541  ispsubcl2N  33588  pclfinclN  33591  ldilval  33754  trlord  34210  cdlemk36  34554  dihlsscpre  34876  baerlem3lem2  35352  baerlem5alem2  35353  baerlem5blem2  35354
  Copyright terms: Public domain W3C validator