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

Theorem 3imp 1147
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 3imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3sylbi 188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3impa  1148  3impb  1149  3impia  1150  3impib  1151  3com23  1159  3an1rs  1165  3imp1  1166  3impd  1167  syl3an2  1218  syl3an3  1219  3jao  1245  biimp3ar  1284  wefrc  4536  sotri2  5222  sotri3  5223  poxp  6417  riotasvdOLD  6552  smo11  6585  oawordri  6752  odi  6781  omass  6782  nndi  6825  nnmass  6826  undifixp  7057  isinf  7281  domunfican  7338  pr2nelem  7844  dfac8alem  7866  fin33i  8205  fin1a2lem10  8245  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  ttukeyg  8353  axdclem  8355  grupr  8628  nqereu  8762  squeeze0  9869  rpnnen1lem5  10560  supxrun  10850  elfznelfzo  11147  injresinj  11155  mulexp  11374  expadd  11377  expmul  11380  bernneq  11460  facdiv  11533  hashgt12el2  11638  leisorel  11664  brfi1uzind  11670  prmfac1  13073  infpnlem1  13233  iscatd2  13861  joinle  14405  meetle  14412  clatleglb  14508  lsmcv  16168  psrvscafval  16409  fiinopn  16929  opnneissb  17133  cnpimaex  17274  regsep  17352  hausnei2  17371  cmpsublem  17416  cmpsub  17417  filufint  17905  blssps  18407  blss  18408  mblsplit  19381  bcmono  21014  2sqlem10  21111  usgraedg4  21359  usgrafisinds  21380  nbgraf1olem3  21406  cusgrasizeinds  21438  cusgrasize2inds  21439  1pthoncl  21545  2pthoncl  21556  wlkdvspthlem  21560  wlkdvspth  21561  3v3e3cycl1  21584  constr3trl  21599  constr3pth  21600  constr3cycl  21601  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  eupatrl  21643  clmgm  21862  grpomndo  21887  zerdivemp1  21975  rngoridfz  21976  chcompl  22698  spansncol  23023  hoaddsub  23272  sconpht  24869  relexpindlem  25092  funpsstri  25335  predpo  25398  imp5p  26204  cntotbnd  26395  rngoneglmul  26457  rngonegrmul  26458  zerdivemp1x  26461  pell14qrexpclnn0  26819  pell1qrgap  26827  aomclem2  27020  rngunsnply  27246  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  hashimarni  27995  swrd0swrd  28009  swrdswrdlem  28010  swrdccatin12lem3a  28021  swrdccatin12b  28027  swrdccat3  28029  uhgraedgrnv  28032  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  usgra2pthlem1  28040  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  usg2wlkonot  28080  usg2wotspth  28081  frgraunss  28099  3cyclfrgrarn1  28116  frgranbnb  28124  vdfrgra0  28126  vdgfrgra0  28127  frgrawopreglem2  28148  frgrawopreglem5  28151  bi33imp12  28287  bi23imp13  28288  bi13imp23  28289  bi23imp1  28292  bi123imp0  28293  ee333  28300  jaoded  28364  3imp31  28365  3imp21  28366  eel12131  28530  eel32131  28533  e333  28554  3imp231  28639  suctrALTcf  28743  suctrALTcfVD  28744  a9e2ndeqALT  28753  bnj600  28996  atlex  29799  cvlexch1  29811  cvlsupr4  29828  cvlsupr5  29829  cvlsupr6  29830  2llnneN  29891  athgt  29938  llnle  30000  lplnle  30022  lvoli2  30063  pmaple  30243  dalawlem10  30362  dalawlem13  30365  dalawlem14  30366  dalaw  30368  lhp2lt  30483  ldilval  30595  cdleme50trn2  31033  cdlemf  31045  cdlemg18b  31161  tendotp  31243  tendospcanN  31506  dihmeetlem3N  31788  dvh4dimlem  31926
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  df-3an 938
  Copyright terms: Public domain W3C validator