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

Theorem imp3a 431
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 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  443  syland  478  imp4c  586  imp4d  587  imp5d  594  expimpd  598  expl  613  3expib  1183  axc9lem1  1944  equs5  2041  sbiedOLD  2101  rsp2  2768  moi  3131  reu6  3137  sbciegft  3205  elpwunsn  3905  prel12  4037  opthpr  4038  invdisj  4269  reusv1  4480  sotr2  4657  wefrc  4701  tz7.7  4732  ordtr2  4750  relop  4977  elres  5133  iss  5142  funssres  5446  fv3  5691  funfvima  5939  isomin  6015  sorpsscmpl  6360  peano5  6488  f1oweALT  6550  poxp  6673  soxp  6674  tfr3  6844  tz7.48-1  6884  omordi  6993  odi  7006  omass  7007  oen0  7013  nndi  7050  nnmass  7051  nnmordi  7058  nnmord  7059  eroveu  7183  findcard3  7543  fiint  7576  suplub  7698  hartogs  7746  card2on  7757  unxpwdom2  7791  inf3lem2  7823  epfrs  7939  tcel  7953  dfac2  8288  cfcoflem  8429  infpssr  8465  isf32lem9  8518  axdc3lem4  8610  axcclem  8614  zorn2lem7  8659  ttukeylem6  8671  brdom6disj  8687  ondomon  8715  inar1  8929  gruen  8966  indpi  9063  nqereu  9085  genpn0  9159  distrlem1pr  9181  distrlem5pr  9183  ltexprlem1  9192  reclem4pr  9206  mulcmpblnr  9228  supsrlem  9265  lelttr  9452  ltletr  9453  ltlen  9463  mulgt1  10175  fzind  10727  eqreznegel  10927  xrlelttr  11117  xrltletr  11118  fzen  11453  elfzodifsumelfzo  11587  bernneq  11973  swrdswrdlem  12336  wrd2ind  12355  swrdccatin1  12357  repsdf2  12399  limsupbnd2  12944  rlimuni  13011  mulcn2  13056  rlimno1  13114  ndvdssub  13593  coprmdvds  13770  coprmdvds2  13771  maxprmfct  13781  pceu  13895  infpnlem1  13953  imasaddfnlem  14448  plelttr  15124  gsumval2a  15491  symgfix2  15900  gsmsymgrfixlem1  15911  psgnunilem4  15982  lsmmod  16151  lsmdisj2  16158  efgrelexlemb  16226  pgpfac1lem5  16553  lindfrn  18091  mdetunilem7  18265  lmss  18743  lmcnp  18749  hausnei2  18798  isnrm2  18803  isnrm3  18804  cmpsublem  18843  2ndcdisj  18901  1stccnp  18907  txcnpi  19022  txlm  19062  tx1stc  19064  fgss2  19288  fgfil  19289  fgcl  19292  ufileu  19333  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem4  19371  fmfnfm  19372  ufilcmp  19446  cnpfcf  19455  alexsubALTlem2  19461  alexsubALTlem4  19463  alexsubALT  19464  tmdgsum2  19508  tsmsxp  19570  prdsxmslem2  19945  ivthlem2  20777  ivthlem3  20778  ovolicc2  20846  volfiniun  20869  dyadmax  20919  ellimc3  21195  dvlip2  21308  dvne0  21324  axcontlem4  23035  usgra2edg  23123  usgrares1  23145  nb3graprlem1  23181  usgrcyclnl1  23348  nvnencycllem  23351  3v3e3cycl1  23352  4cycl4v4e  23374  4cycl4dv4e  23376  gxnn0add  23583  gxadd  23584  gxnn0mul  23586  gxmul  23587  isch3  24466  ocin  24521  shmodsi  24614  spansneleq  24795  stj  25461  atom1d  25579  atcvat2i  25613  chirredlem1  25616  chirredi  25620  mdsymlem3  25631  mdsymlem6  25634  pconcon  26967  cvmsss2  27010  cvmliftlem7  27027  prodmolem2  27294  dfpo2  27411  dfon2lem9  27450  dfon2  27451  wfr3g  27569  frr3g  27613  frrlem11  27626  cgrextend  27885  btwntriv2  27889  btwncomim  27890  btwnexch3  27897  funtransport  27908  ifscgr  27921  colinearxfr  27952  lineext  27953  fscgr  27957  outsideoftr  28006  itg2addnclem3  28286  itg2addnc  28287  areacirc  28330  trer  28352  finminlem  28354  fnessref  28406  fgmin  28432  ismtybndlem  28546  heibor1lem  28549  prtlem17  28863  pellexlem5  29016  pellex  29018  pell1234qrmulcl  29038  pellfundex  29069  ralxfrd2  29980  iswlkg  30128  wwlknred  30198  el2wlkonotot0  30234  erclwwlktr  30328  erclwwlkntr  30344  clwlkfoclwwlk  30361  frg2woteq  30496  numclwwlkovf2ex  30522  frgraregord013  30554  fmptsnd  30564  ldepspr  30713  19.41rg  30957  iunconlem2  31370  bnj849  31617  bj-andnotim  31773  bj-alanim  31804  bj-equs5v  31894  riotasvd  32177  lshpsmreu  32324  atnle  32532  cvratlem  32635  cvrat2  32643  3dim1  32681  2llnjN  32781  2lplnj  32834  linepsubN  32966  pmapsub  32982  paddasslem14  33047  pclfinN  33114  ispsubcl2N  33161  pclfinclN  33164  ldilval  33327  trlord  33783  cdlemk36  34127  dihlsscpre  34449  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927
  Copyright terms: Public domain W3C validator