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  2057  equs5  2146  rsp2  2806  moi  3260  reu6  3266  sbciegft  3336  elpwunsn  4043  prel12  4180  opthpr  4181  invdisj  4415  reusv1  4625  sotr2  4804  wefrc  4848  relop  5005  elres  5160  iss  5172  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  7042  tfr3  7125  tz7.48-1  7168  omordi  7275  odi  7288  omass  7289  oen0  7295  nndi  7332  nnmass  7333  nnmordi  7340  nnmord  7341  eroveu  7466  findcard3  7820  fiint  7854  suplub  7980  hartogs  8059  card2on  8069  unxpwdom2  8103  inf3lem2  8134  epfrs  8214  tcel  8228  dfac2  8559  cfcoflem  8700  infpssr  8736  isf32lem9  8789  axdc3lem4  8881  axcclem  8885  zorn2lem7  8930  ttukeylem6  8942  brdom6disj  8958  ondomon  8986  inar1  9199  gruen  9236  indpi  9331  nqereu  9353  genpn0  9427  distrlem1pr  9449  distrlem5pr  9451  ltexprlem1  9460  reclem4pr  9474  addsrmo  9496  mulsrmo  9497  supsrlem  9534  lelttr  9723  ltletr  9724  ltlen  9734  mulgt1  10463  fzind  11033  eqreznegel  11249  xrlelttr  11453  xrltletr  11454  fzen  11814  elfzodifsumelfzo  11977  bernneq  12395  swrdswrdlem  12800  wrd2ind  12819  reuccats1lem  12821  swrdccatin1  12824  repsdf2  12866  limsupbnd2  13524  limsupbnd2OLD  13525  rlimuni  13592  mulcn2  13637  rlimno1  13695  prodmolem2  13967  ndvdssub  14363  lcmfunsnlem1  14581  lcmfunsnlem2  14584  maxprmfct  14623  coprmdvds  14630  coprmdvds2  14631  pceu  14759  infpnlem1  14817  prmgaplem6  14989  imasaddfnlem  15385  initoeu1  15857  termoeu1  15864  plelttr  16169  gsumval2a  16473  symgfix2  17008  gsmsymgrfixlem1  17019  psgnunilem4  17089  lsmmod  17260  lsmdisj2  17267  efgrelexlemb  17335  pgpfac1lem5  17647  lindfrn  19310  mat1dimcrng  19433  dmatelnd  19452  mdetunilem7  19574  cpmatacl  19671  cpmatmcllem  19673  chfacfisf  19809  chfacfisfcpmat  19810  lmss  20245  lmcnp  20251  hausnei2  20300  isnrm2  20305  isnrm3  20306  cmpsublem  20345  2ndcdisj  20402  1stccnp  20408  txcnpi  20554  txlm  20594  tx1stc  20596  fgss2  20820  fgfil  20821  fgcl  20824  ufileu  20865  rnelfm  20899  fmfnfmlem2  20901  fmfnfmlem4  20903  fmfnfm  20904  ufilcmp  20978  cnpfcf  20987  alexsubALTlem2  20994  alexsubALTlem4  20996  alexsubALT  20997  tmdgsum2  21042  tsmsxp  21100  prdsxmslem2  21475  ivthlem2  22284  ivthlem3  22285  ovolicc2  22353  volfiniun  22377  dyadmax  22433  ellimc3  22711  dvlip2  22824  dvne0  22840  axcontlem4  24843  usgra2edg  24955  usgrares1  24983  nb3graprlem1  25024  iswlkg  25097  usgrcyclnl1  25213  nvnencycllem  25216  3v3e3cycl1  25217  4cycl4v4e  25239  4cycl4dv4e  25241  wwlknred  25296  erclwwlktr  25388  erclwwlkntr  25400  clwlkfoclwwlk  25418  el2wlkonotot0  25445  frg2woteq  25633  numclwwlkovf2ex  25659  frgraregord013  25691  gxnn0add  25847  gxadd  25848  gxnn0mul  25850  gxmul  25851  isch3  26729  ocin  26784  shmodsi  26877  spansneleq  27058  stj  27723  atom1d  27841  atcvat2i  27875  chirredlem1  27878  chirredi  27882  mdsymlem3  27893  mdsymlem6  27896  bnj849  29524  pconcon  29742  cvmsss2  29785  cvmliftlem7  29802  mclsind  29996  dfpo2  30182  dfon2lem9  30224  dfon2  30225  frr3g  30300  frrlem11  30313  cgrextend  30560  btwntriv2  30564  btwncomim  30565  btwnexch3  30572  funtransport  30583  ifscgr  30596  colinearxfr  30627  lineext  30628  fscgr  30632  outsideoftr  30681  trer  30757  finminlem  30759  fnessref  30798  fgmin  30811  bj-andnotim  30956  bj-alanim  30983  bj-equs5v  31112  relowlssretop  31500  poimirlem29  31672  itg2addnclem3  31698  itg2addnc  31699  areacirc  31740  ismtybndlem  31841  heibor1lem  31844  prtlem17  32155  riotasvd  32236  lshpsmreu  32383  atnle  32591  cvratlem  32694  cvrat2  32702  3dim1  32740  2llnjN  32840  2lplnj  32893  linepsubN  33025  pmapsub  33041  paddasslem14  33106  pclfinN  33173  ispsubcl2N  33220  pclfinclN  33223  ldilval  33386  trlord  33844  cdlemk36  34188  dihlsscpre  34510  baerlem3lem2  34986  baerlem5alem2  34987  baerlem5blem2  34988  pellexlem5  35386  pellex  35388  pell1234qrmulcl  35408  pellfundex  35439  relexpmulnn  35939  19.41rg  36553  iunconlem2  36971  nltle2tri  38105  iccpartnel  38141  bgoldbtbnd  38293  ralxfrd2  38379  usgpredgv  38468  usgpredgvALT  38469  nzerooringczr  38831  ldepspr  39025  aacllem  39300
  Copyright terms: Public domain W3C validator