MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imp Structured version   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  4576  sotri2  5263  sotri3  5264  poxp  6458  riotasvdOLD  6593  smo11  6626  oawordri  6793  odi  6822  omass  6823  nndi  6866  nnmass  6867  undifixp  7098  isinf  7322  domunfican  7379  infssuni  7397  pr2nelem  7888  dfac8alem  7910  fin33i  8249  fin1a2lem10  8289  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  ttukeyg  8397  axdclem  8399  grupr  8672  nqereu  8806  squeeze0  9913  rpnnen1lem5  10604  supxrun  10894  elfznelfzo  11192  injresinj  11200  mulexp  11419  expadd  11422  expmul  11425  bernneq  11505  facdiv  11578  hashgt12el2  11683  leisorel  11709  brfi1uzind  11715  prmfac1  13118  infpnlem1  13278  iscatd2  13906  joinle  14450  meetle  14457  clatleglb  14553  lsmcv  16213  psrvscafval  16454  fiinopn  16974  opnneissb  17178  cnpimaex  17320  regsep  17398  hausnei2  17417  cmpsublem  17462  cmpsub  17463  bwth  17473  filufint  17952  blssps  18454  blss  18455  mblsplit  19428  bcmono  21061  2sqlem10  21158  usgraedg4  21406  usgrafisinds  21427  nbgraf1olem3  21453  cusgrasizeinds  21485  cusgrasize2inds  21486  1pthoncl  21592  2pthoncl  21603  wlkdvspthlem  21607  wlkdvspth  21608  3v3e3cycl1  21631  constr3trl  21646  constr3pth  21647  constr3cycl  21648  4cycl4v4e  21653  4cycl4dv  21654  4cycl4dv4e  21655  eupatrl  21690  clmgm  21909  grpomndo  21934  zerdivemp1  22022  rngoridfz  22023  chcompl  22745  spansncol  23070  hoaddsub  23319  sconpht  24916  relexpindlem  25139  funpsstri  25389  predpo  25459  imp5p  26314  cntotbnd  26505  rngoneglmul  26567  rngonegrmul  26568  zerdivemp1x  26571  pell14qrexpclnn0  26929  pell1qrgap  26937  aomclem2  27130  rngunsnply  27355  ubmelfzo  28126  ubmelm1fzo  28127  fzo1fzo0n0  28128  subsubelfzo0  28135  fzofzim  28136  el2fzo  28138  hashimarni  28164  swrd0swrd  28197  swrdswrdlem  28198  swrdccat3  28215  2cshw1lem1  28248  2cshw1lem2  28249  2cshw2lem2  28253  2cshw2lem3  28254  lswrdn0  28260  cshwssizelem2  28281  cshwssizelem3  28282  uhgraedgrnv  28292  usgra2wlkspthlem1  28306  usgra2wlkspth  28308  usgra2pthlem1  28310  usgra2pth  28311  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  el2wlkonotot0  28339  usg2wlkonot  28350  usg2wotspth  28351  frgraunss  28385  3cyclfrgrarn1  28402  frgranbnb  28410  vdfrgra0  28412  vdgfrgra0  28413  frgrawopreglem2  28434  frgrawopreglem5  28437  bi33imp12  28573  bi23imp13  28574  bi13imp23  28575  bi23imp1  28578  bi123imp0  28579  ee333  28589  jaoded  28653  3imp31  28654  3imp21  28655  eel12131  28821  eel32131  28824  e333  28845  3imp231  28930  suctrALTcf  29034  suctrALTcfVD  29035  a9e2ndeqALT  29043  bnj600  29290  atlex  30114  cvlexch1  30126  cvlsupr4  30143  cvlsupr5  30144  cvlsupr6  30145  2llnneN  30206  athgt  30253  llnle  30315  lplnle  30337  lvoli2  30378  pmaple  30558  dalawlem10  30677  dalawlem13  30680  dalawlem14  30681  dalaw  30683  lhp2lt  30798  ldilval  30910  cdleme50trn2  31348  cdlemf  31360  cdlemg18b  31476  tendotp  31558  tendospcanN  31821  dihmeetlem3N  32103  dvh4dimlem  32241
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