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  2820  moi  2950  disji  4013  reusv6OLD  4547  nnsuc  4675  3optocl  4768  sossfld  5122  soisores  5826  isomin  5836  isofrlem  5839  ovmpt2s  5973  ov2gf  5974  ndmovord  6012  poxp  6229  brtpos  6245  dfsmo2  6366  smoiun  6380  smoord  6384  smogt  6386  omeulem1  6582  omeu  6585  oewordi  6591  mapvalg  6784  pmvalg  6785  elmapg  6787  xpdom3  6962  mapdom3  7035  php3  7049  unxpdomlem3  7071  isinf  7078  findcard2  7100  isfinite2  7117  ordiso  7233  cnfcom3clem  7410  r111  7449  tskwe  7585  pr2ne  7637  infxpenlem  7643  dfac8alem  7658  infdif  7837  infdif2  7838  cff1  7886  coflim  7889  cfslbn  7895  cfslb2n  7896  cofsmo  7897  cfsmolem  7898  cfcoflem  7900  fin23lem27  7956  isf32lem9  7989  isf34lem6  8008  axcc2lem  8064  domtriomlem  8070  axdc4lem  8083  zorn2lem2  8126  axdclem2  8149  konigthlem  8192  gchen1  8249  gchen2  8250  gchpwdom  8298  gchaleph  8299  winainflem  8317  tskcard  8405  gruiun  8423  gruen  8436  intgru  8438  grudomon  8441  grur1a  8443  grutsk1  8445  nqereu  8555  nqereq  8561  ltsonq  8595  prlem934  8659  reclem3pr  8675  1re  8839  axsup  8900  ltlen  8924  addid2  8997  recex  9402  lemul1a  9612  ledivmulOLD  9632  lt2msq  9642  fimaxre2  9704  zdiv  10084  zextlt  10088  prime  10094  uzind2  10106  fzind  10112  lbzbi  10308  qbtwnxr  10529  qextltlem  10531  xralrple  10534  xltneg  10546  xlt2add  10582  supxrgtmnf  10650  ixxub  10679  ixxlb  10680  ioo0  10683  ico0  10704  ioc0  10705  icc0  10706  iocssre  10731  icossre  10732  iccssre  10733  fzen  10813  expclzlem  11129  expaddz  11148  expmulz  11150  hashgadd  11361  ccatopth2  11465  shftuz  11566  cau3lem  11840  caubnd  11844  climuni  12028  lo1resb  12040  o1resb  12042  o1of2  12088  o1add  12089  o1mul  12090  o1sub  12091  eflt  12399  znnenlem  12492  moddvds  12540  dvdscmulr  12559  dvdsmulcr  12560  dvdsle  12576  divalglem8  12601  divalgb  12605  ndvdssub  12608  bitsfzo  12628  gcdcllem1  12692  gcdcllem3  12694  dvdsgcd  12724  isprm3  12769  coprm  12781  qredeu  12788  prmdvdsexpr  12797  prmexpb  12798  eulerthlem2  12852  fermltl  12854  coprimeprodsq  12864  pythagtrip  12889  pcprendvds  12895  pcpremul  12898  pcdvdsb  12923  pc2dvds  12933  4sqlem12  13005  4sqlem18  13011  vdwlem10  13039  xpslem  13477  ismred  13506  mrieqv2d  13543  iscatd  13577  isfuncd  13741  poslubd  14253  dirtr  14360  ghmrn  14698  mndodcongi  14860  oddvdsnn0  14861  oddvds  14864  odcl2  14880  odhash3  14889  gexdvds  14897  pgpfi  14918  lsmss1b  14978  lsmss2b  14980  efgsrel  15045  efgred  15059  cntzcmn  15138  cyggenod  15173  lt6abl  15183  gsumcom2  15228  pgpfac1lem2  15312  pgpfac1lem3  15314  dvdsunit  15447  unitmulclb  15449  irredrmul  15491  isabvd  15587  lmodvsdi  15652  lss0cl  15706  islbs3  15910  lbsextlem2  15914  mvrf1  16172  xrsdsreclblem  16419  opnnei  16859  neindisj2  16862  cncls2  17004  cncls  17005  cnntr  17006  cnpresti  17018  cnprest  17019  lmcnp  17034  isreg2  17107  ordthauslem  17113  uncon  17157  2ndc1stc  17179  kgen2ss  17252  ptclsg  17311  cnmptcom  17374  kqfvima  17423  hmeof1o  17457  fbncp  17536  fbfinnfr  17538  trfbas2  17540  isufil2  17605  ufprim  17606  trufil  17607  filufint  17617  hausflim  17678  flimrest  17680  flimcls  17682  cnpfcf  17738  alexsubALT  17747  tmdgsum  17780  opnsubg  17792  cldsubg  17795  divstgpopn  17804  tsmsxp  17839  blpnf  17956  blss  17974  blssec  17983  neibl  18049  prdsxmslem2  18077  xrsmopn  18320  metnrm  18368  climcncf  18406  iccpnfhmeo  18445  xrhmeo  18446  bndth  18458  cphsqrcl3  18625  iscau2  18705  iscmet3lem2  18720  bcthlem5  18752  bcth3  18755  ishl2  18789  ivthlem1  18813  cmmbl  18894  iundisj2  18908  voliunlem2  18910  mbfaddlem  19017  itg2itg1  19093  itg2seq  19099  itg2mulclem  19103  cnplimc  19239  dvres2  19264  deg1nn0clb  19478  deg1lt0  19479  deg1ge  19486  plypf1  19596  plyadd  19601  plymul  19602  coeeu  19609  dgrub2  19619  coeidlem  19621  coeid3  19624  coemullem  19633  coe11  19636  coemulhi  19637  coemulc  19638  dgreq0  19648  dgrlt  19649  dgradd2  19651  vieta1lem2  19693  sineq0  19891  tanord1  19901  tanord  19902  cxpeq0  20027  cxpmul2z  20040  cxpcn3lem  20089  angpieqvd  20130  o1cxp  20271  scvxcvx  20282  chtublem  20452  bposlem3  20527  lgsqr  20587  dchrisumlema  20639  dchrisumlem2  20641  ostth2lem3  20786  lpni  20848  gxnn0neg  20932  gxnn0suc  20933  gxcl  20934  gxneg  20935  gxcom  20938  gxinv  20939  gxsuc  20941  gxnn0add  20943  gxadd  20944  gxnn0mul  20946  gxmul  20947  ipasslem5  21415  htthlem  21499  omlsii  21984  spansni  22138  spansneleq  22151  elspansn4  22154  sumspansn  22230  homco1  22383  homulass  22384  mdsl0  22892  ssdmd1  22895  ssdmd2  22896  cvdmd  22919  chirredlem2  22973  atdmd  22980  atmd2  22982  isoun  23244  iocinioc2  23274  disjif  23357  disjif2  23360  iundisj2fi  23366  iundisj2f  23368  logccne0  23399  measinblem  23549  measres  23551  measdivcstOLD  23553  measdivcst  23554  mbfmco2  23572  indpi1  23607  orvclteinc  23678  cvmlift2lem10  23845  ghomf1olem  24003  nodense  24345  dfrdg4  24490  brbtwn2  24535  axpasch  24571  axcontlem4  24597  axcontlem5  24598  brcolinear2  24683  brsegle2  24734  limsucncmpi  24886  ee7.2aOLD  24902  areacirc  24942  rspc2edv  24974  uninqs  25050  domintreflemb  25073  injsurinj  25160  repcpwti  25172  cbcpcp  25173  prl1  25179  oriso  25225  ubos  25267  curgrpact  25383  ltrran2  25414  ltrooo  25415  fldi  25438  svli2  25495  elioo1t3  25513  intopcoaconb  25551  limptlimpr2lem2  25586  islimrs4  25593  lvsovso  25637  negveud  25679  negveudr  25680  clsmulrv  25694  intvconlem1  25714  cmpassoh  25812  issrc  25878  clscnc  26021  isconcl6a  26114  nn0prpw  26250  ntruni  26256  clsint2  26258  fnessref  26304  fnemeet2  26327  fnejoin2  26329  filbcmb  26443  mettrifi  26484  heiborlem8  26553  heiborlem10  26555  heibor  26556  riscer  26630  igenval2  26702  oddcomabszz  27040  jm2.19lem4  27096  fiuneneq  27524  idomsubgmo  27525  addrcom  27691  stoweidlem26  27786  stoweidlem34  27794  int3  28446  suctrALTcf  28771  suctrALT3  28773  suctrALT4  28777  chordthmALT  28783  bnj605  29012  bnj607  29021  bnj964  29048  bnj1033  29072  bnj1128  29093  bnj1137  29098  bnj1136  29100  bnj1413  29138  bnj60  29165  lshpcmp  29251  eqlkr  29362  lkrlsp2  29366  lkrshp  29368  cvrnbtwn2  29538  cvlexch3  29595  cvlexch4N  29596  cvlatexchb1  29597  cvlsupr3  29607  exatleN  29666  cvratlem  29683  atcvrj2b  29694  cvrat3  29704  cvrat4  29705  athgt  29718  ps-1  29739  ps-2  29740  3atlem5  29749  3at  29752  llnneat  29776  llnmlplnN  29801  lplnneat  29807  lplnnelln  29808  islpln2a  29810  lplnriaN  29812  lplnribN  29813  lplnexllnN  29826  2llnjaN  29828  lvolnle3at  29844  lvolneatN  29850  lvolnelln  29851  lvolnelpln  29852  islvol2aN  29854  dalem62  29996  pmapglb2N  30033  pmapglb2xN  30034  lncmp  30045  paddasslem14  30095  paddasslem15  30096  pmod2iN  30111  hlmod1i  30118  pclfinclN  30212  osumcllem8N  30225  pexmidlem4N  30235  pl42lem1N  30241  pl42lem4N  30244  lhpexle1  30270  lhpexle2lem  30271  lhpmcvr5N  30289  lhpmcvr6N  30290  ltrneq  30411  trlnidatb  30439  cdleme0ex2N  30486  cdleme27a  30629  cdleme17d3  30758  cdlemeg46gfre  30794  cdleme48gfv1  30798  cdlemeg49lebilem  30801  cdlemf2  30824  cdlemf  30825  cdlemfnid  30826  trlord  30831  cdlemg31c  30961  cdlemg35  30975  trlcone  30990  tendoeq2  31036  cdlemj3  31085  cdlemk26b-3  31167  cdlemk33N  31171  cdleml3N  31240  cdlemn  31475  dih1dimb2  31504  dihord5apre  31525  dihmeetlem1N  31553  dihglblem5apreN  31554  dihglblem2N  31557  dihglblem3N  31558  dihmeetlem13N  31582  dihmeetlem15N  31584  dihatexv  31601  hdmap14lem12  32145
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