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

Theorem imp3a 420
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 75 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 418 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 27 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp32  422  pm3.31  432  syland  467  imp4c  574  imp4d  575  imp5d  582  expimpd  586  expl  601  3expib  1154  equs5  1936  sbied  1976  rsp2  2605  moi  2948  reu6  2954  sbciegft  3021  prel12  3789  opthpr  3790  invdisj  4012  sotr2  4343  wefrc  4387  tz7.7  4418  ordtr2  4436  reusv1  4534  elpwunsn  4568  peano5  4679  relop  4834  elres  4990  iss  4998  funssres  5294  fv3  5541  funfvima  5753  isomin  5834  f1oweALT  5851  poxp  6227  soxp  6228  sorpsscmpl  6288  riotasvd  6347  tfrlem2  6392  tfr3  6415  tz7.48-1  6455  omordi  6564  odi  6577  omass  6578  oen0  6584  nndi  6621  nnmass  6622  nnmordi  6629  nnmord  6630  eroveu  6753  findcard3  7100  fiint  7133  suplub  7211  hartogs  7259  card2on  7268  unxpwdom2  7302  inf3lem2  7330  epfrs  7413  tcel  7430  dfac2  7757  cfcoflem  7898  infpssr  7934  isf32lem9  7987  axdc3lem4  8079  axcclem  8083  zorn2lem7  8129  ttukeylem6  8141  brdom6disj  8157  ondomon  8185  inar1  8397  gruen  8434  indpi  8531  nqereu  8553  genpn0  8627  distrlem1pr  8649  distrlem5pr  8651  ltexprlem1  8660  reclem4pr  8674  mulcmpblnr  8696  supsrlem  8733  lelttr  8912  ltletr  8913  ltlen  8922  mulgt1  9615  fzind  10110  eqreznegel  10303  xrlelttr  10487  xrltletr  10488  fzen  10811  bernneq  11227  limsupbnd2  11957  rlimuni  12024  mulcn2  12069  rlimno1  12127  ndvdssub  12606  coprmdvds  12781  coprmdvds2  12782  maxprmfct  12792  pceu  12899  infpnlem1  12957  imasaddfnlem  13430  iscatd  13575  plelttr  14106  spwmo  14335  gsumval2a  14459  lsmmod  14984  lsmdisj2  14991  efgrelexlemb  15059  pgpfac1lem5  15314  lmodvsdi2OLD  15653  lmodvsassOLD  15655  lmss  17026  lmcnp  17032  hausnei2  17081  isnrm2  17086  isnrm3  17087  cmpsublem  17126  2ndcdisj  17182  1stccnp  17188  txcnpi  17302  txlm  17342  tx1stc  17344  fgss2  17569  fgfil  17570  fgcl  17573  ufileu  17614  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  ufilcmp  17727  cnpfcf  17736  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  tmdgsum2  17779  tsmsxp  17837  prdsxmslem2  18075  ivthlem2  18812  ivthlem3  18813  ovolicc2  18881  volfiniun  18904  dyadmax  18953  ellimc3  19229  dvlip2  19342  dvne0  19358  gxnn0add  20941  gxadd  20942  gxnn0mul  20944  gxmul  20945  isch3  21821  ocin  21875  shmodsi  21968  spansneleq  22149  stj  22815  atom1d  22933  atcvat2i  22967  chirredlem1  22970  chirredi  22974  mdsymlem3  22985  mdsymlem6  22988  pconcon  23762  cvmsss2  23805  cvmliftlem7  23822  dfpo2  24112  dfon2lem9  24147  dfon2  24148  wfr3g  24255  frr3g  24280  frrlem11  24293  axcontlem4  24595  cgrextend  24631  btwntriv2  24635  btwncomim  24636  btwnexch3  24643  funtransport  24654  ifscgr  24667  colinearxfr  24698  lineext  24699  fscgr  24703  outsideoftr  24752  areacirc  24931  ffvelrnb  25131  dffprod  25319  trooo  25394  intopcoaconb  25540  qusp  25542  clscnc  26010  trer  26227  finminlem  26231  fnessref  26293  fgmin  26319  ismtybndlem  26530  heibor1lem  26533  prtlem17  26744  pellexlem5  26918  pellex  26920  pell1234qrmulcl  26940  pellfundex  26971  lindfrn  27291  psgnunilem4  27420  19.41rg  28316  bnj849  28957  a12study  29132  a12studyALT  29133  a12study3  29135  lshpsmreu  29299  atnle  29507  cvratlem  29610  cvrat2  29618  3dim1  29656  2llnjN  29756  2lplnj  29809  linepsubN  29941  pmapsub  29957  paddasslem14  30022  pclfinN  30089  ispsubcl2N  30136  pclfinclN  30139  ldilval  30302  trlord  30758  cdlemk36  31102  dihlsscpre  31424  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902
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 177  df-an 360
  Copyright terms: Public domain W3C validator