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

Theorem 3imp 1145
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
3imp  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 3imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3sylbi 187 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3impa  1146  3impb  1147  3impia  1148  3impib  1149  3com23  1157  3an1rs  1163  3imp1  1164  3impd  1165  syl3an2  1216  syl3an3  1217  3jao  1243  biimp3ar  1282  wefrc  4403  sotri2  5088  sotri3  5089  poxp  6243  riotasvdOLD  6364  smo11  6397  oawordri  6564  odi  6593  omass  6594  nndi  6637  nnmass  6638  undifixp  6868  isinf  7092  domunfican  7145  pr2nelem  7650  dfac8alem  7672  fin33i  8011  fin1a2lem10  8051  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  ttukeyg  8160  axdclem  8162  grupr  8435  nqereu  8569  squeeze0  9675  rpnnen1lem5  10362  supxrun  10650  mulexp  11157  expadd  11160  expmul  11163  bernneq  11243  facdiv  11316  leisorel  11414  prmfac1  12813  infpnlem1  12973  iscatd2  13599  joinle  14143  meetle  14150  clatleglb  14246  lmodvsdi2OLD  15669  lmodvsassOLD  15671  lsmcv  15910  psrvscafval  16151  fiinopn  16663  opnneissb  16867  cnpimaex  17002  regsep  17078  hausnei2  17097  cmpsublem  17142  cmpsub  17143  filufint  17631  blss  17988  mblsplit  18907  bcmono  20532  2sqlem10  20629  clmgm  21004  grpomndo  21029  chcompl  21838  spansncol  22163  hoaddsub  22412  sconpht  23775  relexpindlem  24051  funpsstri  24192  predpo  24255  and4as  25042  rspc2edv  25066  isunscov  25177  eqfnung2  25221  mapmapmap  25251  prl  25270  prl2  25272  prjmapcp2  25273  dfps2  25392  iscomb  25437  clfsebsr  25452  multinv  25525  multinvb  25526  zerdivemp1  25539  rngoridfz  25540  svs2  25590  truni3  25610  unint2t  25621  intopcoaconlem3b  25641  fisub  25657  cmptdst  25671  limptlimpr2lem2  25678  islimrs3  25684  islimrs4  25685  bwt2  25695  flfneicn  25728  lvsovso  25729  lvsovso2  25730  negveud  25771  negveudr  25772  issubcv  25773  clsmulcv  25785  distsava  25792  hdrmp  25809  cmpassoh  25904  imonclem  25916  ismonc  25917  cmpmon  25918  icmpmon  25919  iepiclem  25926  isepic  25927  propsrc  25971  tartarmap  25991  cmpmor  26078  clscnc  26113  pgapspf2  26156  lppotos  26247  bosser  26270  pdiveql  26271  imp5p  26323  cntotbnd  26623  rngoneglmul  26685  rngonegrmul  26686  zerdivemp1x  26689  pell14qrexpclnn0  27054  pell1qrgap  27062  aomclem2  27255  rngunsnply  27481  elfznelfzo  28213  injresinj  28215  hashgt12el2  28219  wlkdvspthlem  28365  wlkdvspth  28366  eupatrl  28385  3v3e3cycl1  28390  constr3trl  28405  constr3pth  28406  constr3cycl  28407  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  3cyclfrgrarn1  28435  bi33imp12  28554  bi23imp13  28555  bi13imp23  28556  bi13imp2  28557  bi12imp3  28558  bi23imp1  28559  bi123imp0  28560  ee333  28567  jaoded  28631  3imp31  28632  3imp21  28633  eel12131  28798  eel32131  28801  e333  28822  3imp231  28907  suctrALTcf  29014  suctrALTcfVD  29015  a9e2ndeqALT  29024  bnj600  29267  atlex  30128  cvlexch1  30140  cvlsupr4  30157  cvlsupr5  30158  cvlsupr6  30159  2llnneN  30220  athgt  30267  llnle  30329  lplnle  30351  lvoli2  30392  pmaple  30572  dalawlem10  30691  dalawlem13  30694  dalawlem14  30695  dalaw  30697  lhp2lt  30812  ldilval  30924  cdleme50trn2  31362  cdlemf  31374  cdlemg18b  31490  tendotp  31572  tendospcanN  31835  dihmeetlem3N  32117  dvh4dimlem  32255
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  df-3an 936
  Copyright terms: Public domain W3C validator