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

Theorem impd 429
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 427 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 31 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  imp32  431  pm3.31  443  syland  479  imp4c  589  imp4d  590  imp5d  597  expimpd  601  expl  616  3expib  1197  axc9lem1  2006  equs5  2094  rsp2  2828  moi  3279  reu6  3285  sbciegft  3355  elpwunsn  4057  prel12  4193  opthpr  4194  invdisj  4428  reusv1  4637  sotr2  4818  wefrc  4862  tz7.7  4893  ordtr2  4911  relop  5142  elres  5297  iss  5309  funssres  5610  fv3  5861  fmptsnd  6069  tpres  6100  funfvima  6122  isomin  6208  sorpsscmpl  6564  peano5  6696  f1oweALT  6757  poxp  6885  soxp  6886  tfr3  7060  tz7.48-1  7100  omordi  7207  odi  7220  omass  7221  oen0  7227  nndi  7264  nnmass  7265  nnmordi  7272  nnmord  7273  eroveu  7398  findcard3  7755  fiint  7789  suplub  7911  hartogs  7961  card2on  7972  unxpwdom2  8006  inf3lem2  8037  epfrs  8153  tcel  8167  dfac2  8502  cfcoflem  8643  infpssr  8679  isf32lem9  8732  axdc3lem4  8824  axcclem  8828  zorn2lem7  8873  ttukeylem6  8885  brdom6disj  8901  ondomon  8929  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  10397  fzind  10958  eqreznegel  11168  xrlelttr  11362  xrltletr  11363  fzen  11706  elfzodifsumelfzo  11863  bernneq  12277  swrdswrdlem  12678  wrd2ind  12697  reuccats1lem  12699  swrdccatin1  12702  repsdf2  12744  limsupbnd2  13391  rlimuni  13458  mulcn2  13503  rlimno1  13561  prodmolem2  13827  ndvdssub  14152  coprmdvds  14330  coprmdvds2  14331  maxprmfct  14341  pceu  14457  infpnlem1  14515  imasaddfnlem  15020  initoeu1  15492  termoeu1  15499  plelttr  15804  gsumval2a  16108  symgfix2  16643  gsmsymgrfixlem1  16654  psgnunilem4  16724  lsmmod  16895  lsmdisj2  16902  efgrelexlemb  16970  pgpfac1lem5  17328  lindfrn  19026  mat1dimcrng  19149  dmatelnd  19168  mdetunilem7  19290  cpmatacl  19387  cpmatmcllem  19389  chfacfisf  19525  chfacfisfcpmat  19526  lmss  19969  lmcnp  19975  hausnei2  20024  isnrm2  20029  isnrm3  20030  cmpsublem  20069  2ndcdisj  20126  1stccnp  20132  txcnpi  20278  txlm  20318  tx1stc  20320  fgss2  20544  fgfil  20545  fgcl  20548  ufileu  20589  rnelfm  20623  fmfnfmlem2  20625  fmfnfmlem4  20627  fmfnfm  20628  ufilcmp  20702  cnpfcf  20711  alexsubALTlem2  20717  alexsubALTlem4  20719  alexsubALT  20720  tmdgsum2  20764  tsmsxp  20826  prdsxmslem2  21201  ivthlem2  22033  ivthlem3  22034  ovolicc2  22102  volfiniun  22126  dyadmax  22176  ellimc3  22452  dvlip2  22565  dvne0  22581  axcontlem4  24475  usgra2edg  24587  usgrares1  24615  nb3graprlem1  24656  iswlkg  24729  usgrcyclnl1  24845  nvnencycllem  24848  3v3e3cycl1  24849  4cycl4v4e  24871  4cycl4dv4e  24873  wwlknred  24928  erclwwlktr  25020  erclwwlkntr  25032  clwlkfoclwwlk  25050  el2wlkonotot0  25077  frg2woteq  25265  numclwwlkovf2ex  25291  frgraregord013  25323  gxnn0add  25477  gxadd  25478  gxnn0mul  25480  gxmul  25481  isch3  26360  ocin  26415  shmodsi  26508  spansneleq  26689  stj  27355  atom1d  27473  atcvat2i  27507  chirredlem1  27510  chirredi  27514  mdsymlem3  27525  mdsymlem6  27528  pconcon  28943  cvmsss2  28986  cvmliftlem7  29003  mclsind  29197  dfpo2  29428  dfon2lem9  29466  dfon2  29467  wfr3g  29585  frr3g  29629  frrlem11  29642  cgrextend  29889  btwntriv2  29893  btwncomim  29894  btwnexch3  29901  funtransport  29912  ifscgr  29925  colinearxfr  29956  lineext  29957  fscgr  29961  outsideoftr  30010  itg2addnclem3  30311  itg2addnc  30312  areacirc  30355  trer  30377  finminlem  30379  fnessref  30418  fgmin  30431  ismtybndlem  30545  heibor1lem  30548  prtlem17  30860  pellexlem5  31011  pellex  31013  pell1234qrmulcl  31033  pellfundex  31064  ralxfrd2  32696  usgpredgv  32790  usgpredgvALT  32791  nzerooringczr  33153  ldepspr  33347  aacllem  33623  19.41rg  33736  iunconlem2  34155  bnj849  34403  bj-andnotim  34597  bj-alanim  34624  bj-equs5v  34752  riotasvd  35103  lshpsmreu  35250  atnle  35458  cvratlem  35561  cvrat2  35569  3dim1  35607  2llnjN  35707  2lplnj  35760  linepsubN  35892  pmapsub  35908  paddasslem14  35973  pclfinN  36040  ispsubcl2N  36087  pclfinclN  36090  ldilval  36253  trlord  36711  cdlemk36  37055  dihlsscpre  37377  baerlem3lem2  37853  baerlem5alem2  37854  baerlem5blem2  37855  relexpmulnn  38248
  Copyright terms: Public domain W3C validator