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  1949  sbied  1989  rsp2  2618  moi  2961  reu6  2967  sbciegft  3034  prel12  3805  opthpr  3806  invdisj  4028  sotr2  4359  wefrc  4403  tz7.7  4434  ordtr2  4452  reusv1  4550  elpwunsn  4584  peano5  4695  relop  4850  elres  5006  iss  5014  funssres  5310  fv3  5557  funfvima  5769  isomin  5850  f1oweALT  5867  poxp  6243  soxp  6244  sorpsscmpl  6304  riotasvd  6363  tfrlem2  6408  tfr3  6431  tz7.48-1  6471  omordi  6580  odi  6593  omass  6594  oen0  6600  nndi  6637  nnmass  6638  nnmordi  6645  nnmord  6646  eroveu  6769  findcard3  7116  fiint  7149  suplub  7227  hartogs  7275  card2on  7284  unxpwdom2  7318  inf3lem2  7346  epfrs  7429  tcel  7446  dfac2  7773  cfcoflem  7914  infpssr  7950  isf32lem9  8003  axdc3lem4  8095  axcclem  8099  zorn2lem7  8145  ttukeylem6  8157  brdom6disj  8173  ondomon  8201  inar1  8413  gruen  8450  indpi  8547  nqereu  8569  genpn0  8643  distrlem1pr  8665  distrlem5pr  8667  ltexprlem1  8676  reclem4pr  8690  mulcmpblnr  8712  supsrlem  8749  lelttr  8928  ltletr  8929  ltlen  8938  mulgt1  9631  fzind  10126  eqreznegel  10319  xrlelttr  10503  xrltletr  10504  fzen  10827  bernneq  11243  limsupbnd2  11973  rlimuni  12040  mulcn2  12085  rlimno1  12143  ndvdssub  12622  coprmdvds  12797  coprmdvds2  12798  maxprmfct  12808  pceu  12915  infpnlem1  12973  imasaddfnlem  13446  iscatd  13591  plelttr  14122  spwmo  14351  gsumval2a  14475  lsmmod  15000  lsmdisj2  15007  efgrelexlemb  15075  pgpfac1lem5  15330  lmodvsdi2OLD  15669  lmodvsassOLD  15671  lmss  17042  lmcnp  17048  hausnei2  17097  isnrm2  17102  isnrm3  17103  cmpsublem  17142  2ndcdisj  17198  1stccnp  17204  txcnpi  17318  txlm  17358  tx1stc  17360  fgss2  17585  fgfil  17586  fgcl  17589  ufileu  17630  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  ufilcmp  17743  cnpfcf  17752  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  tmdgsum2  17795  tsmsxp  17853  prdsxmslem2  18091  ivthlem2  18828  ivthlem3  18829  ovolicc2  18897  volfiniun  18920  dyadmax  18969  ellimc3  19245  dvlip2  19358  dvne0  19374  gxnn0add  20957  gxadd  20958  gxnn0mul  20960  gxmul  20961  isch3  21837  ocin  21891  shmodsi  21984  spansneleq  22165  stj  22831  atom1d  22949  atcvat2i  22983  chirredlem1  22986  chirredi  22990  mdsymlem3  23001  mdsymlem6  23004  pconcon  23777  cvmsss2  23820  cvmliftlem7  23837  prodmolem2  24158  prodmo  24159  dfpo2  24183  dfon2lem9  24218  dfon2  24219  wfr3g  24326  frr3g  24351  frrlem11  24364  axcontlem4  24667  cgrextend  24703  btwntriv2  24707  btwncomim  24708  btwnexch3  24715  funtransport  24726  ifscgr  24739  colinearxfr  24770  lineext  24771  fscgr  24775  outsideoftr  24824  itg2addnc  25005  areacirc  25034  ffvelrnb  25234  dffprod  25422  trooo  25497  intopcoaconb  25643  qusp  25645  clscnc  26113  trer  26330  finminlem  26334  fnessref  26396  fgmin  26422  ismtybndlem  26633  heibor1lem  26636  prtlem17  26847  pellexlem5  27021  pellex  27023  pell1234qrmulcl  27043  pellfundex  27074  lindfrn  27394  psgnunilem4  27523  nb3graprlem1  28287  usgrcyclnl1  28386  nvnencycllem  28389  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  19.41rg  28615  bnj849  29273  equs5NEW7  29509  sbiedNEW7  29515  a12study  29754  a12studyALT  29755  a12study3  29757  lshpsmreu  29921  atnle  30129  cvratlem  30232  cvrat2  30240  3dim1  30278  2llnjN  30378  2lplnj  30431  linepsubN  30563  pmapsub  30579  paddasslem14  30644  pclfinN  30711  ispsubcl2N  30758  pclfinclN  30761  ldilval  30924  trlord  31380  cdlemk36  31724  dihlsscpre  32046  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524
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