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  2049  sbied  2085  rsp2  2728  moi  3077  reu6  3083  sbciegft  3151  prel12  3935  opthpr  3936  invdisj  4161  sotr2  4492  wefrc  4536  tz7.7  4567  ordtr2  4585  reusv1  4682  elpwunsn  4716  peano5  4827  relop  4982  elres  5140  iss  5148  funssres  5452  fv3  5703  funfvima  5932  isomin  6016  f1oweALT  6033  poxp  6417  soxp  6418  sorpsscmpl  6492  riotasvd  6551  tfrlem2  6596  tfr3  6619  tz7.48-1  6659  omordi  6768  odi  6781  omass  6782  oen0  6788  nndi  6825  nnmass  6826  nnmordi  6833  nnmord  6834  eroveu  6958  findcard3  7309  fiint  7342  suplub  7421  hartogs  7469  card2on  7478  unxpwdom2  7512  inf3lem2  7540  epfrs  7623  tcel  7640  dfac2  7967  cfcoflem  8108  infpssr  8144  isf32lem9  8197  axdc3lem4  8289  axcclem  8293  zorn2lem7  8338  ttukeylem6  8350  brdom6disj  8366  ondomon  8394  inar1  8606  gruen  8643  indpi  8740  nqereu  8762  genpn0  8836  distrlem1pr  8858  distrlem5pr  8860  ltexprlem1  8869  reclem4pr  8883  mulcmpblnr  8905  supsrlem  8942  lelttr  9121  ltletr  9122  ltlen  9131  mulgt1  9825  fzind  10324  eqreznegel  10517  xrlelttr  10702  xrltletr  10703  fzen  11028  bernneq  11460  limsupbnd2  12232  rlimuni  12299  mulcn2  12344  rlimno1  12402  ndvdssub  12882  coprmdvds  13057  coprmdvds2  13058  maxprmfct  13068  pceu  13175  infpnlem1  13233  imasaddfnlem  13708  plelttr  14384  spwmo  14613  gsumval2a  14737  lsmmod  15262  lsmdisj2  15269  efgrelexlemb  15337  pgpfac1lem5  15592  lmss  17316  lmcnp  17322  hausnei2  17371  isnrm2  17376  isnrm3  17377  cmpsublem  17416  2ndcdisj  17472  1stccnp  17478  txcnpi  17593  txlm  17633  tx1stc  17635  fgss2  17859  fgfil  17860  fgcl  17863  ufileu  17904  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  ufilcmp  18017  cnpfcf  18026  alexsubALTlem2  18032  alexsubALTlem4  18034  alexsubALT  18035  tmdgsum2  18079  tsmsxp  18137  prdsxmslem2  18512  ivthlem2  19302  ivthlem3  19303  ovolicc2  19371  volfiniun  19394  dyadmax  19443  ellimc3  19719  dvlip2  19832  dvne0  19848  usgra2edg  21355  usgrares1  21377  nb3graprlem1  21413  usgrcyclnl1  21580  nvnencycllem  21583  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  gxnn0add  21815  gxadd  21816  gxnn0mul  21818  gxmul  21819  isch3  22697  ocin  22751  shmodsi  22844  spansneleq  23025  stj  23691  atom1d  23809  atcvat2i  23843  chirredlem1  23846  chirredi  23850  mdsymlem3  23861  mdsymlem6  23864  pconcon  24871  cvmsss2  24914  cvmliftlem7  24931  prodmolem2  25214  dfpo2  25326  dfon2lem9  25361  dfon2  25362  wfr3g  25469  frr3g  25494  frrlem11  25507  axcontlem4  25810  cgrextend  25846  btwntriv2  25850  btwncomim  25851  btwnexch3  25858  funtransport  25869  ifscgr  25882  colinearxfr  25913  lineext  25914  fscgr  25918  outsideoftr  25967  itg2addnclem3  26157  itg2addnc  26158  areacirc  26187  trer  26209  finminlem  26211  fnessref  26263  fgmin  26289  ismtybndlem  26405  heibor1lem  26408  prtlem17  26615  pellexlem5  26786  pellex  26788  pell1234qrmulcl  26808  pellfundex  26839  lindfrn  27159  psgnunilem4  27288  swrdswrdlem  28010  swrdccatin1  28016  el2wlkonotot0  28069  frg2woteq  28163  19.41rg  28348  bnj849  29002  equs5NEW7  29238  sbiedNEW7  29244  lshpsmreu  29592  atnle  29800  cvratlem  29903  cvrat2  29911  3dim1  29949  2llnjN  30049  2lplnj  30102  linepsubN  30234  pmapsub  30250  paddasslem14  30315  pclfinN  30382  ispsubcl2N  30429  pclfinclN  30432  ldilval  30595  trlord  31051  cdlemk36  31395  dihlsscpre  31717  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195
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