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

Theorem 3expa 1151
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expa  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anidm23  1241  mp3an2  1265  mpd3an3  1278  rgen3  2640  moi2  2946  sbc3ie  3060  preq12bg  3791  reuhypd  4561  f1imass  5788  fcof1o  5803  weisoeq  5853  curry1f  6212  curry2f  6214  riota5OLD  6331  f1ofveu  6339  f1ocnvfv3  6340  tfrlem11  6404  oalimcl  6558  oeordsuc  6592  oelim2  6593  nneob  6650  mapxpen  7027  findcard  7097  wemaplem3  7263  en2eqpr  7637  infxpabs  7838  infxp  7841  cfflb  7885  cfsmolem  7896  isf32lem12  7990  fin1a2lem9  8034  fin1a2s  8040  axcc3  8064  axdc3lem4  8079  zornn0g  8132  pwfseqlem4  8284  tskwun  8406  tskint  8407  tskxp  8409  tskmap  8410  gruf  8433  gruwun  8435  grutsk1  8443  addcanpi  8523  ltapi  8527  mul4  8981  add4  9027  2addsub  9065  addsubeq4  9066  muladd  9212  ltleadd  9257  receu  9413  p1le  9599  lemul12b  9613  lbinfm  9707  zdiv  10082  fzind  10110  fnn0ind  10111  uzss  10248  zbtwnre  10314  qmulcl  10334  qreccl  10336  xrlttr  10474  xaddass  10569  xmulasslem3  10606  xmulass  10607  xadddilem  10614  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  ixxin  10673  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  iooshf  10728  prunioo  10764  ioojoin  10766  elfz5  10790  fzind2  10923  mulexpz  11142  expsub  11149  digit2  11234  digit1  11235  facndiv  11301  faclbnd4lem4  11309  faclbnd4  11310  faclbnd5  11311  bccmpl  11322  bcval5  11330  bcpasc  11333  swrdccat1  11460  swrdccat2  11461  cats1un  11476  crim  11600  absmax  11813  ello12r  11991  elo12r  12002  climshftlem  12048  2sumeq2dv  12178  expcnv  12322  rpnnen2lem7  12499  dvdsval3  12535  dvdsnegb  12546  muldvds1  12553  muldvds2  12554  dvdscmul  12555  dvdsmulc  12556  dvdsmulcr  12558  dvds2ln  12559  divalgb  12603  ndvdssub  12606  gcddiv  12728  rpexp1i  12800  phiprmpw  12844  pythagtriplem1  12869  pockthg  12953  infpnlem1  12957  4sqlem3  12997  0ramcl  13070  firest  13337  imasaddfnlem  13430  imasleval  13443  xpsfrn2  13472  mrerintcl  13499  iscatd  13575  lubid  14116  clatleglb  14230  mreclat  14290  pslem  14315  grplmulf1o  14542  grplactcnv  14564  mulgnn0subcl  14580  mulgsubcl  14581  mulgdir  14592  issubg2  14636  cycsubgcl  14643  cycsubgss  14644  nmzsubg  14658  eqgen  14670  ghmmulg  14695  conjghm  14713  odeq  14865  odval2  14866  odf1  14875  dfod2  14877  gexdvds  14895  gexdvds2  14896  gexcl2  14900  gexdvds3  14901  sylow2blem2  14932  efgsp1  15046  efgrelexlemb  15059  mulgmhm  15127  mulgghm  15128  iscyggen2  15168  iscyg3  15173  rnglghm  15388  rngrghm  15389  gsumdixp  15392  dvdsrcl2  15432  crngunit  15444  subrgugrp  15564  cntzsubr  15577  lmodvsdir  15652  lmodvsass  15654  lmodvsghm  15686  lsssubg  15714  lss1d  15720  islbs2  15907  issubgrpd2  15941  lidlsubg  15967  divscrng  15992  lpigen  16008  xrsdsreval  16416  expghm  16450  mulgghm2  16459  ip0r  16541  obs2ss  16629  elcls2  16811  opnnei  16857  innei  16862  cnpnei  16993  iscncl  16998  cnconst  17012  ordthauslem  17111  1stccnp  17188  llyrest  17211  nllyrest  17212  kgenss  17238  xkoccn  17313  kqsat  17422  kqt0lem  17427  isr0  17428  fbssfi  17532  isfild  17553  filcon  17578  trfilss  17584  fgtr  17585  ufileu  17614  ufilen  17625  fmfnfmlem4  17652  fmfnfm  17653  hausflimi  17675  cnpflf2  17695  cnpflf  17696  cnflf  17697  cnpfcf  17736  cnfcf  17737  tmdmulg  17775  clsnsg  17792  tsmsxplem1  17835  tsmsxp  17837  ismeti  17890  isxmet2d  17892  elbl2  17950  xblpnf  17953  xbln0  17965  blin  17970  blssex  17973  blsscls2  18050  blcls  18052  blsscls  18053  metss  18054  metrest  18070  metcn  18089  nmf2  18115  nmdvr  18181  nmoi  18237  nmoix  18238  nmoleub  18240  nghmcn  18254  xrsxmet  18315  iccntr  18326  metdsle  18356  icoopnst  18437  iocopnst  18438  icccvx  18448  pi1xfr  18553  lmmbr  18684  lmmbr2  18685  iscfil3  18699  iscau2  18703  cfilres  18722  bcthlem1  18746  bcthlem4  18749  bcthlem5  18750  ioombl  18922  iccvolcl  18924  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  dvmptfsum  19322  ig1pcl  19561  ig1prsp  19563  aannenlem1  19708  taylplem1  19742  dvtaylp  19749  relogeftb  19938  logdivlt  19972  cxpexp  20015  rpcxpcl  20023  isppw2  20353  vmappw  20354  lgslem4  20538  lgscllem  20542  lgsneg1  20559  lgsne0  20572  grpoidinvlem3  20873  isvci  21138  nmcvcn  21268  ipval2lem2  21277  ipval2lem5  21283  sspival  21314  sspimsval  21316  isblo2  21361  nmoo0  21369  blocni  21383  isph  21400  sspph  21433  hvadd4  21615  hiassdi  21670  ocsh  21862  chj4  22114  spansncol  22147  pjjsi  22279  hoscl  22325  hodcl  22327  hoadd4  22364  homco1  22381  homulass  22382  hoadddi  22383  hoadddir  22384  unoplin  22500  adjvalval  22517  hmoplin  22522  bralnfn  22528  brafnmul  22531  lnopmi  22580  lnopcoi  22583  hmops  22600  hmopm  22601  nmophmi  22611  lnfncnbd  22637  cnlnadjlem2  22648  adjlnop  22666  adjmul  22672  adjadd  22673  branmfn  22685  kbass5  22700  kbass6  22701  leop2  22704  leopadd  22712  leopmuli  22713  pjimai  22756  atcvatlem  22965  chirredlem2  22971  mdsymlem3  22985  mdsymlem5  22987  sumdmdii  22995  sumdmdlem  22998  cdj3lem2a  23016  cdj3lem2b  23017  cdj3lem3a  23019  cdj3i  23021  ballotlemirc  23090  xreceu  23105  abfmpeld  23218  abfmpel  23219  hasheuni  23453  txpcon  23763  cvmscld  23804  dfrdg2  24152  nobndlem8  24353  brbtwn2  24533  ax5seglem1  24556  ax5seglem2  24557  axcontlem4  24595  segconeu  24634  linecom  24773  linethru  24776  lineintmo  24780  areacirclem4  24927  areacirclem5  24929  areacirclem6  24930  areacirc  24931  cmprtr  25396  cmpltr2  25407  cmperltr  25409  iscnp4  25563  cmp2morp  25958  cmpmor  25975  fnemeet2  26316  fnejoin2  26318  infmrlbOLD  26422  fzmul  26443  subspopn  26466  isbndx  26506  isbnd2  26507  isbnd3  26508  ssbnd  26512  prdstotbnd  26518  heibor1  26534  rrnmet  26553  rngonegmn1l  26580  rngohomco  26605  rngoisocnv  26612  rngoisoco  26613  crngohomfo  26631  isidlc  26640  rngoidl  26649  prnc  26692  ispridlc  26695  oddcomabszz  27029  acongtr  27065  rpnnen3lem  27124  islssfg  27168  lmhmfgsplit  27184  unxpwdom3  27256  islindf3  27296  hbtlem7  27329  sdrgacs  27509  hashgcdeq  27517  dvconstbi  27551  ioovolcl  27742  bnj1204  29042  cvrval2  29464  glbconxN  29567  hlrelat5N  29590  cvratlem  29610  cvrat2  29618  athgt  29645  3dim2  29657  llnn0  29705  lplnn0N  29736  lvoln0N  29780  snatpsubN  29939  paddasslem18  30026  pmod1i  30037  lhpexle2  30199  lhpexle3lem  30200  lhpexle3  30201  ldilcnv  30304  trlcnv  30354  trlnidatb  30366  cdleme32snaw  30624  cdleme32fvaw  30628  cdleme42ke  30674  cdlemeg46gf  30722  cdleme50trn12  30741  cdlemg1cex  30777  cdlemb3  30795  tgrpgrplem  30938  tgrpabl  30940  tendoplcl2  30967  tendo0pl  30980  tendoicl  30985  tendoipl  30986  cdlemkid3N  31122  tendoex  31164  erngdvlem4  31180  erngdvlem4-rN  31188  dib1dim  31355  dib1dim2  31358  dihglbcpreN  31490  dihmeetALTN  31517  dih1dimatlem  31519  dihatlat  31524
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