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

Theorem 3expia 1153
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expia  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mp3an3  1266  3gencl  2894  moi  3024  disji  4092  reusv6OLD  4627  nnsuc  4755  3optocl  4848  sossfld  5202  soisores  5911  isomin  5921  isofrlem  5924  ovmpt2s  6058  ov2gf  6059  ndmovord  6097  poxp  6314  brtpos  6330  dfsmo2  6451  smoiun  6465  smoord  6469  smogt  6471  omeulem1  6667  omeu  6670  oewordi  6676  uniinqs  6826  mapvalg  6870  pmvalg  6871  elmapg  6873  xpdom3  7048  mapdom3  7121  php3  7135  unxpdomlem3  7157  isinf  7164  findcard2  7188  isfinite2  7205  ordiso  7321  cnfcom3clem  7498  r111  7537  tskwe  7673  pr2ne  7725  infxpenlem  7731  dfac8alem  7746  infdif  7925  infdif2  7926  cff1  7974  coflim  7977  cfslbn  7983  cfslb2n  7984  cofsmo  7985  cfsmolem  7986  cfcoflem  7988  fin23lem27  8044  isf32lem9  8077  isf34lem6  8096  axcc2lem  8152  domtriomlem  8158  axdc4lem  8171  zorn2lem2  8214  axdclem2  8237  konigthlem  8280  gchen1  8337  gchen2  8338  gchpwdom  8386  gchaleph  8387  winainflem  8405  tskcard  8493  gruiun  8511  gruen  8524  intgru  8526  grudomon  8529  grur1a  8531  grutsk1  8533  nqereu  8643  nqereq  8649  ltsonq  8683  prlem934  8747  reclem3pr  8763  1re  8927  axsup  8988  ltlen  9012  addid2  9085  recex  9490  lemul1a  9700  ledivmulOLD  9720  lt2msq  9730  fimaxre2  9792  zdiv  10174  zextlt  10178  prime  10184  uzind2  10196  fzind  10202  lbzbi  10398  qbtwnxr  10619  qextltlem  10621  xralrple  10624  xltneg  10636  xlt2add  10672  supxrgtmnf  10740  ixxub  10769  ixxlb  10770  ioo0  10773  ico0  10794  ioc0  10795  icc0  10796  iocssre  10821  icossre  10822  iccssre  10823  fzen  10903  expclzlem  11220  expaddz  11239  expmulz  11241  hashgadd  11452  ccatopth2  11559  shftuz  11660  cau3lem  11934  caubnd  11938  climuni  12122  lo1resb  12134  o1resb  12136  o1of2  12182  o1add  12183  o1mul  12184  o1sub  12185  eflt  12494  znnenlem  12587  moddvds  12635  dvdscmulr  12654  dvdsmulcr  12655  dvdsle  12671  divalglem8  12696  divalgb  12700  ndvdssub  12703  bitsfzo  12723  gcdcllem1  12787  gcdcllem3  12789  dvdsgcd  12819  isprm3  12864  coprm  12876  qredeu  12883  prmdvdsexpr  12892  prmexpb  12893  eulerthlem2  12947  fermltl  12949  coprimeprodsq  12959  pythagtrip  12984  pcprendvds  12990  pcpremul  12993  pcdvdsb  13018  pc2dvds  13028  4sqlem12  13100  4sqlem18  13106  vdwlem10  13134  xpslem  13574  ismred  13603  mrieqv2d  13640  iscatd  13674  isfuncd  13838  poslubd  14350  dirtr  14457  ghmrn  14795  mndodcongi  14957  oddvdsnn0  14958  oddvds  14961  odcl2  14977  odhash3  14986  gexdvds  14994  pgpfi  15015  lsmss1b  15075  lsmss2b  15077  efgsrel  15142  efgred  15156  cntzcmn  15235  cyggenod  15270  lt6abl  15280  gsumcom2  15325  pgpfac1lem2  15409  pgpfac1lem3  15411  dvdsunit  15544  unitmulclb  15546  irredrmul  15588  isabvd  15684  lmodvsdi  15749  lss0cl  15803  islbs3  16007  lbsextlem2  16011  mvrf1  16269  xrsdsreclblem  16523  opnnei  16963  neindisj2  16966  cncls2  17108  cncls  17109  cnntr  17110  cnpresti  17122  cnprest  17123  lmcnp  17138  isreg2  17211  ordthauslem  17217  uncon  17261  2ndc1stc  17283  kgen2ss  17356  ptclsg  17415  cnmptcom  17478  kqfvima  17527  hmeof1o  17561  fbncp  17636  fbfinnfr  17638  trfbas2  17640  isufil2  17705  ufprim  17706  trufil  17707  filufint  17717  hausflim  17778  flimrest  17780  flimcls  17782  cnpfcf  17838  alexsubALT  17847  tmdgsum  17880  opnsubg  17892  cldsubg  17895  divstgpopn  17904  tsmsxp  17939  blpnf  18056  blss  18074  blssec  18083  neibl  18149  prdsxmslem2  18177  xrsmopn  18420  metnrm  18469  climcncf  18507  iccpnfhmeo  18547  xrhmeo  18548  bndth  18560  cphsqrcl3  18727  iscau2  18807  iscmet3lem2  18822  bcthlem5  18854  bcth3  18857  ishl2  18891  ivthlem1  18915  cmmbl  18996  iundisj2  19010  voliunlem2  19012  mbfaddlem  19119  itg2itg1  19195  itg2seq  19201  itg2mulclem  19205  cnplimc  19341  dvres2  19366  deg1nn0clb  19580  deg1lt0  19581  deg1ge  19588  plypf1  19698  plyadd  19703  plymul  19704  coeeu  19711  dgrub2  19721  coeidlem  19723  coeid3  19726  coemullem  19735  coe11  19738  coemulhi  19739  coemulc  19740  dgreq0  19750  dgrlt  19751  dgradd2  19753  vieta1lem2  19795  sineq0  19996  tanord1  20006  tanord  20007  cxpeq0  20136  cxpmul2z  20149  cxpcn3lem  20198  angpieqvd  20239  o1cxp  20380  scvxcvx  20391  chtublem  20562  bposlem3  20637  lgsqr  20697  dchrisumlema  20749  dchrisumlem2  20751  ostth2lem3  20896  lpni  20958  gxnn0neg  21042  gxnn0suc  21043  gxcl  21044  gxneg  21045  gxcom  21048  gxinv  21049  gxsuc  21051  gxnn0add  21053  gxadd  21054  gxnn0mul  21056  gxmul  21057  ipasslem5  21527  htthlem  21611  omlsii  22096  spansni  22250  spansneleq  22263  elspansn4  22266  sumspansn  22342  homco1  22495  homulass  22496  mdsl0  23004  ssdmd1  23007  ssdmd2  23008  cvdmd  23031  chirredlem2  23085  atdmd  23092  atmd2  23094  disjif  23219  disjif2  23222  iundisj2f  23228  isoun  23293  iocinioc2  23344  iundisj2fi  23357  logccne0  23661  indpi1  23685  measinblem  23838  measres  23840  measdivcstOLD  23842  measdivcst  23843  mbfmco2  23879  orvclteinc  23982  cvmlift2lem10  24247  ghomf1olem  24405  ntrivcvgmul  24531  nodense  24901  dfrdg4  25047  brbtwn2  25092  axpasch  25128  axcontlem4  25154  axcontlem5  25155  brcolinear2  25240  brsegle2  25291  limsucncmpi  25443  ee7.2aOLD  25459  areacirc  25523  nn0prpw  25563  ntruni  25569  clsint2  25571  fnessref  25617  fnemeet2  25640  fnejoin2  25642  filbcmb  25756  mettrifi  25797  heiborlem8  25865  heiborlem10  25867  heibor  25868  riscer  25942  igenval2  26014  oddcomabszz  26352  jm2.19lem4  26408  fiuneneq  26836  idomsubgmo  26837  addrcom  27003  stoweidlem26  27098  stoweidlem34  27106  sizeusglecusg  27649  int3  28135  suctrALTcf  28460  suctrALT3  28462  suctrALT4  28466  chordthmALT  28472  bnj605  28701  bnj607  28710  bnj964  28737  bnj1033  28761  bnj1128  28782  bnj1137  28787  bnj1136  28789  bnj1413  28827  bnj60  28854  lshpcmp  29247  eqlkr  29358  lkrlsp2  29362  lkrshp  29364  cvrnbtwn2  29534  cvlexch3  29591  cvlexch4N  29592  cvlatexchb1  29593  cvlsupr3  29603  exatleN  29662  cvratlem  29679  atcvrj2b  29690  cvrat3  29700  cvrat4  29701  athgt  29714  ps-1  29735  ps-2  29736  3atlem5  29745  3at  29748  llnneat  29772  llnmlplnN  29797  lplnneat  29803  lplnnelln  29804  islpln2a  29806  lplnriaN  29808  lplnribN  29809  lplnexllnN  29822  2llnjaN  29824  lvolnle3at  29840  lvolneatN  29846  lvolnelln  29847  lvolnelpln  29848  islvol2aN  29850  dalem62  29992  pmapglb2N  30029  pmapglb2xN  30030  lncmp  30041  paddasslem14  30091  paddasslem15  30092  pmod2iN  30107  hlmod1i  30114  pclfinclN  30208  osumcllem8N  30221  pexmidlem4N  30231  pl42lem1N  30237  pl42lem4N  30240  lhpexle1  30266  lhpexle2lem  30267  lhpmcvr5N  30285  lhpmcvr6N  30286  ltrneq  30407  trlnidatb  30435  cdleme0ex2N  30482  cdleme27a  30625  cdleme17d3  30754  cdlemeg46gfre  30790  cdleme48gfv1  30794  cdlemeg49lebilem  30797  cdlemf2  30820  cdlemf  30821  cdlemfnid  30822  trlord  30827  cdlemg31c  30957  cdlemg35  30971  trlcone  30986  tendoeq2  31032  cdlemj3  31081  cdlemk26b-3  31163  cdlemk33N  31167  cdleml3N  31236  cdlemn  31471  dih1dimb2  31500  dihord5apre  31521  dihmeetlem1N  31549  dihglblem5apreN  31550  dihglblem2N  31553  dihglblem3N  31554  dihmeetlem13N  31578  dihmeetlem15N  31580  dihatexv  31597  hdmap14lem12  32141
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