MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp3a Structured version   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  2085  sbiedOLD  2124  rsp2  2760  moi  3109  reu6  3115  sbciegft  3183  prel12  3967  opthpr  3968  invdisj  4193  sotr2  4524  wefrc  4568  tz7.7  4599  ordtr2  4617  reusv1  4715  elpwunsn  4749  peano5  4860  relop  5015  elres  5173  iss  5181  funssres  5485  fv3  5736  funfvima  5965  isomin  6049  f1oweALT  6066  poxp  6450  soxp  6451  sorpsscmpl  6525  riotasvd  6584  tfrlem2  6629  tfr3  6652  tz7.48-1  6692  omordi  6801  odi  6814  omass  6815  oen0  6821  nndi  6858  nnmass  6859  nnmordi  6866  nnmord  6867  eroveu  6991  findcard3  7342  fiint  7375  suplub  7457  hartogs  7505  card2on  7514  unxpwdom2  7548  inf3lem2  7576  epfrs  7659  tcel  7676  dfac2  8003  cfcoflem  8144  infpssr  8180  isf32lem9  8233  axdc3lem4  8325  axcclem  8329  zorn2lem7  8374  ttukeylem6  8386  brdom6disj  8402  ondomon  8430  inar1  8642  gruen  8679  indpi  8776  nqereu  8798  genpn0  8872  distrlem1pr  8894  distrlem5pr  8896  ltexprlem1  8905  reclem4pr  8919  mulcmpblnr  8941  supsrlem  8978  lelttr  9157  ltletr  9158  ltlen  9167  mulgt1  9861  fzind  10360  eqreznegel  10553  xrlelttr  10738  xrltletr  10739  fzen  11064  bernneq  11497  limsupbnd2  12269  rlimuni  12336  mulcn2  12381  rlimno1  12439  ndvdssub  12919  coprmdvds  13094  coprmdvds2  13095  maxprmfct  13105  pceu  13212  infpnlem1  13270  imasaddfnlem  13745  plelttr  14421  spwmo  14650  gsumval2a  14774  lsmmod  15299  lsmdisj2  15306  efgrelexlemb  15374  pgpfac1lem5  15629  lmss  17354  lmcnp  17360  hausnei2  17409  isnrm2  17414  isnrm3  17415  cmpsublem  17454  2ndcdisj  17511  1stccnp  17517  txcnpi  17632  txlm  17672  tx1stc  17674  fgss2  17898  fgfil  17899  fgcl  17902  ufileu  17943  rnelfm  17977  fmfnfmlem2  17979  fmfnfmlem4  17981  fmfnfm  17982  ufilcmp  18056  cnpfcf  18065  alexsubALTlem2  18071  alexsubALTlem4  18073  alexsubALT  18074  tmdgsum2  18118  tsmsxp  18176  prdsxmslem2  18551  ivthlem2  19341  ivthlem3  19342  ovolicc2  19410  volfiniun  19433  dyadmax  19482  ellimc3  19758  dvlip2  19871  dvne0  19887  usgra2edg  21394  usgrares1  21416  nb3graprlem1  21452  usgrcyclnl1  21619  nvnencycllem  21622  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv4e  21647  gxnn0add  21854  gxadd  21855  gxnn0mul  21857  gxmul  21858  isch3  22736  ocin  22790  shmodsi  22883  spansneleq  23064  stj  23730  atom1d  23848  atcvat2i  23882  chirredlem1  23885  chirredi  23889  mdsymlem3  23900  mdsymlem6  23903  pconcon  24910  cvmsss2  24953  cvmliftlem7  24970  prodmolem2  25253  dfpo2  25370  dfon2lem9  25410  dfon2  25411  wfr3g  25529  frr3g  25573  frrlem11  25586  axcontlem4  25898  cgrextend  25934  btwntriv2  25938  btwncomim  25939  btwnexch3  25946  funtransport  25957  ifscgr  25970  colinearxfr  26001  lineext  26002  fscgr  26006  outsideoftr  26055  itg2addnclem3  26248  itg2addnc  26249  areacirc  26278  trer  26300  finminlem  26302  fnessref  26354  fgmin  26380  ismtybndlem  26496  heibor1lem  26499  prtlem17  26706  pellexlem5  26877  pellex  26879  pell1234qrmulcl  26899  pellfundex  26930  lindfrn  27249  psgnunilem4  27378  ralxfrd2  28049  swrdswrdlem  28154  swrdccatin1  28161  el2wlkonotot0  28282  frg2woteq  28376  19.41rg  28564  iunconlem2  28974  bnj849  29223  equs5NEW7  29461  sbiedNEW7  29467  lshpsmreu  29834  atnle  30042  cvratlem  30145  cvrat2  30153  3dim1  30191  2llnjN  30291  2lplnj  30344  linepsubN  30476  pmapsub  30492  paddasslem14  30557  pclfinN  30624  ispsubcl2N  30671  pclfinclN  30674  ldilval  30837  trlord  31293  cdlemk36  31637  dihlsscpre  31959  baerlem3lem2  32435  baerlem5alem2  32436  baerlem5blem2  32437
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