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

Theorem imp3a 421
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp3a  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem imp3a
StepHypRef Expression
1 imp3.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3l 77 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 419 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 29 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp32  423  pm3.31  433  syland  468  imp4c  575  imp4d  576  imp5d  583  expimpd  587  expl  602  3expib  1156  equs5  2035  sbied  2071  rsp2  2713  moi  3062  reu6  3068  sbciegft  3136  prel12  3919  opthpr  3920  invdisj  4144  sotr2  4475  wefrc  4519  tz7.7  4550  ordtr2  4568  reusv1  4665  elpwunsn  4699  peano5  4810  relop  4965  elres  5123  iss  5131  funssres  5435  fv3  5686  funfvima  5914  isomin  5998  f1oweALT  6015  poxp  6396  soxp  6397  sorpsscmpl  6471  riotasvd  6530  tfrlem2  6575  tfr3  6598  tz7.48-1  6638  omordi  6747  odi  6760  omass  6761  oen0  6767  nndi  6804  nnmass  6805  nnmordi  6812  nnmord  6813  eroveu  6937  findcard3  7288  fiint  7321  suplub  7400  hartogs  7448  card2on  7457  unxpwdom2  7491  inf3lem2  7519  epfrs  7602  tcel  7619  dfac2  7946  cfcoflem  8087  infpssr  8123  isf32lem9  8176  axdc3lem4  8268  axcclem  8272  zorn2lem7  8317  ttukeylem6  8329  brdom6disj  8345  ondomon  8373  inar1  8585  gruen  8622  indpi  8719  nqereu  8741  genpn0  8815  distrlem1pr  8837  distrlem5pr  8839  ltexprlem1  8848  reclem4pr  8862  mulcmpblnr  8884  supsrlem  8921  lelttr  9100  ltletr  9101  ltlen  9110  mulgt1  9803  fzind  10302  eqreznegel  10495  xrlelttr  10680  xrltletr  10681  fzen  11006  bernneq  11434  limsupbnd2  12206  rlimuni  12273  mulcn2  12318  rlimno1  12376  ndvdssub  12856  coprmdvds  13031  coprmdvds2  13032  maxprmfct  13042  pceu  13149  infpnlem1  13207  imasaddfnlem  13682  plelttr  14358  spwmo  14587  gsumval2a  14711  lsmmod  15236  lsmdisj2  15243  efgrelexlemb  15311  pgpfac1lem5  15566  lmss  17286  lmcnp  17292  hausnei2  17341  isnrm2  17346  isnrm3  17347  cmpsublem  17386  2ndcdisj  17442  1stccnp  17448  txcnpi  17563  txlm  17603  tx1stc  17605  fgss2  17829  fgfil  17830  fgcl  17833  ufileu  17874  rnelfm  17908  fmfnfmlem2  17910  fmfnfmlem4  17912  fmfnfm  17913  ufilcmp  17987  cnpfcf  17996  alexsubALTlem2  18002  alexsubALTlem4  18004  alexsubALT  18005  tmdgsum2  18049  tsmsxp  18107  prdsxmslem2  18451  ivthlem2  19218  ivthlem3  19219  ovolicc2  19287  volfiniun  19310  dyadmax  19359  ellimc3  19635  dvlip2  19748  dvne0  19764  usgra2edg  21270  usgrares1  21292  nb3graprlem1  21328  usgrcyclnl1  21477  nvnencycllem  21480  3v3e3cycl1  21481  4cycl4v4e  21503  4cycl4dv4e  21505  gxnn0add  21712  gxadd  21713  gxnn0mul  21715  gxmul  21716  isch3  22594  ocin  22648  shmodsi  22741  spansneleq  22922  stj  23588  atom1d  23706  atcvat2i  23740  chirredlem1  23743  chirredi  23747  mdsymlem3  23758  mdsymlem6  23761  pconcon  24699  cvmsss2  24742  cvmliftlem7  24759  prodmolem2  25042  dfpo2  25138  dfon2lem9  25173  dfon2  25174  wfr3g  25281  frr3g  25306  frrlem11  25319  axcontlem4  25622  cgrextend  25658  btwntriv2  25662  btwncomim  25663  btwnexch3  25670  funtransport  25681  ifscgr  25694  colinearxfr  25725  lineext  25726  fscgr  25730  outsideoftr  25779  itg2addnc  25961  areacirc  25990  trer  26012  finminlem  26014  fnessref  26066  fgmin  26092  ismtybndlem  26208  heibor1lem  26211  prtlem17  26418  pellexlem5  26589  pellex  26591  pell1234qrmulcl  26611  pellfundex  26642  lindfrn  26962  psgnunilem4  27091  19.41rg  27982  bnj849  28636  equs5NEW7  28872  sbiedNEW7  28878  lshpsmreu  29226  atnle  29434  cvratlem  29537  cvrat2  29545  3dim1  29583  2llnjN  29683  2lplnj  29736  linepsubN  29868  pmapsub  29884  paddasslem14  29949  pclfinN  30016  ispsubcl2N  30063  pclfinclN  30066  ldilval  30229  trlord  30685  cdlemk36  31029  dihlsscpre  31351  baerlem3lem2  31827  baerlem5alem2  31828  baerlem5blem2  31829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator