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

Theorem 3expia 1155
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 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mp3an3  1268  3gencl  2946  moi  3077  disji  4160  reusv6OLD  4693  nnsuc  4821  3optocl  4913  sossfld  5276  soisores  6006  isomin  6016  isofrlem  6019  ovmpt2s  6156  ov2gf  6157  ndmovord  6196  poxp  6417  brtpos  6447  dfsmo2  6568  smoiun  6582  smoord  6586  smogt  6588  omeulem1  6784  omeu  6787  oewordi  6793  uniinqs  6943  mapvalg  6987  pmvalg  6988  elmapg  6990  xpdom3  7165  mapdom3  7238  php3  7252  unxpdomlem3  7274  isinf  7281  findcard2  7307  isfinite2  7324  ordiso  7441  cnfcom3clem  7618  r111  7657  tskwe  7793  pr2ne  7845  infxpenlem  7851  dfac8alem  7866  infdif  8045  infdif2  8046  cff1  8094  coflim  8097  cfslbn  8103  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  fin23lem27  8164  isf32lem9  8197  isf34lem6  8216  axcc2lem  8272  domtriomlem  8278  axdc4lem  8291  zorn2lem2  8333  axdclem2  8356  konigthlem  8399  gchen1  8456  gchen2  8457  gchpwdom  8505  gchaleph  8506  winainflem  8524  tskcard  8612  gruiun  8630  gruen  8643  intgru  8645  grudomon  8648  grur1a  8650  grutsk1  8652  nqereu  8762  nqereq  8768  ltsonq  8802  prlem934  8866  reclem3pr  8882  1re  9046  axsup  9107  ltlen  9131  addid2  9205  recex  9610  lemul1a  9820  ledivmulOLD  9840  lt2msq  9850  fimaxre2  9912  zdiv  10296  zextlt  10300  prime  10306  uzind2  10318  fzind  10324  lbzbi  10520  qbtwnxr  10742  qextltlem  10744  xralrple  10747  xltneg  10759  xlt2add  10795  supxrgtmnf  10864  ixxub  10893  ixxlb  10894  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  iocssre  10946  icossre  10947  iccssre  10948  fzen  11028  expclzlem  11360  expaddz  11379  expmulz  11381  hashgadd  11606  ccatopth2  11732  shftuz  11839  cau3lem  12113  caubnd  12117  climuni  12301  lo1resb  12313  o1resb  12315  o1of2  12361  o1add  12362  o1mul  12363  o1sub  12364  eflt  12673  znnenlem  12766  moddvds  12814  dvdscmulr  12833  dvdsmulcr  12834  dvdsle  12850  divalglem8  12875  divalgb  12879  ndvdssub  12882  bitsfzo  12902  gcdcllem1  12966  gcdcllem3  12968  dvdsgcd  12998  isprm3  13043  coprm  13055  qredeu  13062  prmdvdsexpr  13071  prmexpb  13072  eulerthlem2  13126  fermltl  13128  coprimeprodsq  13138  pythagtrip  13163  pcprendvds  13169  pcpremul  13172  pcdvdsb  13197  pc2dvds  13207  4sqlem12  13279  4sqlem18  13285  vdwlem10  13313  xpslem  13753  ismred  13782  mrieqv2d  13819  iscatd  13853  isfuncd  14017  poslubd  14529  dirtr  14636  ghmrn  14974  mndodcongi  15136  oddvdsnn0  15137  oddvds  15140  odcl2  15156  odhash3  15165  gexdvds  15173  pgpfi  15194  lsmss1b  15254  lsmss2b  15256  efgsrel  15321  efgred  15335  cntzcmn  15414  cyggenod  15449  lt6abl  15459  gsumcom2  15504  pgpfac1lem2  15588  pgpfac1lem3  15590  dvdsunit  15723  unitmulclb  15725  irredrmul  15767  isabvd  15863  lmodvsdi  15928  lss0cl  15978  islbs3  16182  lbsextlem2  16186  mvrf1  16444  xrsdsreclblem  16699  opnnei  17139  neindisj2  17142  cncls2  17291  cncls  17292  cnntr  17293  cnpresti  17306  cnprest  17307  lmcnp  17322  isreg2  17395  ordthauslem  17401  uncon  17445  2ndc1stc  17467  kgen2ss  17540  ptclsg  17600  cnmptcom  17663  kqfvima  17715  hmeof1o  17749  fbncp  17824  fbfinnfr  17826  trfbas2  17828  isufil2  17893  ufprim  17894  trufil  17895  filufint  17905  hausflim  17966  flimrest  17968  flimcls  17970  cnpfcf  18026  alexsubALT  18035  tmdgsum  18078  opnsubg  18090  cldsubg  18093  divstgpopn  18102  tsmsxp  18137  blpnf  18380  blssps  18407  blss  18408  blssec  18418  neibl  18484  prdsxmslem2  18512  xrsmopn  18796  metnrm  18845  climcncf  18883  iccpnfhmeo  18923  xrhmeo  18924  bndth  18936  cphsqrcl3  19103  iscau2  19183  iscmet3lem2  19198  bcthlem5  19234  bcth3  19237  ishl2  19277  ivthlem1  19301  cmmbl  19382  iundisj2  19396  voliunlem2  19398  mbfaddlem  19505  itg2itg1  19581  itg2seq  19587  itg2mulclem  19591  cnplimc  19727  dvres2  19752  deg1nn0clb  19966  deg1lt0  19967  deg1ge  19974  plypf1  20084  plyadd  20089  plymul  20090  coeeu  20097  dgrub2  20107  coeidlem  20109  coeid3  20112  coemullem  20121  coe11  20124  coemulhi  20125  coemulc  20126  dgreq0  20136  dgrlt  20137  dgradd2  20139  vieta1lem2  20181  sineq0  20382  tanord1  20392  tanord  20393  cxpeq0  20522  cxpmul2z  20535  cxpcn3lem  20584  angpieqvd  20625  o1cxp  20766  scvxcvx  20777  chtublem  20948  bposlem3  21023  lgsqr  21083  dchrisumlema  21135  dchrisumlem2  21137  ostth2lem3  21282  sizeusglecusg  21448  lpni  21720  gxnn0neg  21804  gxnn0suc  21805  gxcl  21806  gxneg  21807  gxcom  21810  gxinv  21811  gxsuc  21813  gxnn0add  21815  gxadd  21816  gxnn0mul  21818  gxmul  21819  ipasslem5  22289  htthlem  22373  omlsii  22858  spansni  23012  spansneleq  23025  elspansn4  23028  sumspansn  23104  homco1  23257  homulass  23258  mdsl0  23766  ssdmd1  23769  ssdmd2  23770  cvdmd  23793  chirredlem2  23847  atdmd  23854  atmd2  23856  disjif  23973  iundisj2f  23983  isoun  24042  iocinioc2  24095  iundisj2fi  24106  logccne0  24349  indpi1  24372  measinblem  24527  measres  24529  measdivcstOLD  24531  mbfmco2  24568  orvclteinc  24686  cvmlift2lem10  24952  ghomf1olem  25058  ntrivcvgmul  25183  nodense  25557  dfrdg4  25703  brbtwn2  25748  axpasch  25784  axcontlem4  25810  axcontlem5  25811  brcolinear2  25896  brsegle2  25947  limsucncmpi  26099  ee7.2aOLD  26115  areacirc  26187  nn0prpw  26216  ntruni  26220  clsint2  26222  fnessref  26263  fnemeet2  26286  fnejoin2  26288  filbcmb  26332  mettrifi  26353  heiborlem8  26417  heiborlem10  26419  heibor  26420  riscer  26494  igenval2  26566  oddcomabszz  26897  jm2.19lem4  26953  fiuneneq  27381  idomsubgmo  27382  addrcom  27547  stoweidlem26  27642  stoweidlem34  27650  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  int3  28422  suctrALTcf  28743  suctrALT3  28745  chordthmALT  28755  bnj605  28984  bnj607  28993  bnj964  29020  bnj1033  29044  bnj1128  29065  bnj1137  29070  bnj1136  29072  bnj1413  29110  bnj60  29137  lshpcmp  29471  eqlkr  29582  lkrlsp2  29586  lkrshp  29588  cvrnbtwn2  29758  cvlexch3  29815  cvlexch4N  29816  cvlatexchb1  29817  cvlsupr3  29827  exatleN  29886  cvratlem  29903  atcvrj2b  29914  cvrat3  29924  cvrat4  29925  athgt  29938  ps-1  29959  ps-2  29960  3atlem5  29969  3at  29972  llnneat  29996  llnmlplnN  30021  lplnneat  30027  lplnnelln  30028  islpln2a  30030  lplnriaN  30032  lplnribN  30033  lplnexllnN  30046  2llnjaN  30048  lvolnle3at  30064  lvolneatN  30070  lvolnelln  30071  lvolnelpln  30072  islvol2aN  30074  dalem62  30216  pmapglb2N  30253  pmapglb2xN  30254  lncmp  30265  paddasslem14  30315  paddasslem15  30316  pmod2iN  30331  hlmod1i  30338  pclfinclN  30432  osumcllem8N  30445  pexmidlem4N  30455  pl42lem1N  30461  pl42lem4N  30464  lhpexle1  30490  lhpexle2lem  30491  lhpmcvr5N  30509  lhpmcvr6N  30510  ltrneq  30631  trlnidatb  30659  cdleme0ex2N  30706  cdleme27a  30849  cdleme17d3  30978  cdlemeg46gfre  31014  cdleme48gfv1  31018  cdlemeg49lebilem  31021  cdlemf2  31044  cdlemf  31045  cdlemfnid  31046  trlord  31051  cdlemg31c  31181  cdlemg35  31195  trlcone  31210  tendoeq2  31256  cdlemj3  31305  cdlemk26b-3  31387  cdlemk33N  31391  cdleml3N  31460  cdlemn  31695  dih1dimb2  31724  dihord5apre  31745  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem2N  31777  dihglblem3N  31778  dihmeetlem13N  31802  dihmeetlem15N  31804  dihatexv  31821  hdmap14lem12  32365
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