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

Theorem 3exp2 1172
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Assertion
Ref Expression
3exp2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
21ex 425 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
323expd 1171 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anassrs  1176  po2nr  4518  fliftfund  6037  frfi  7354  fin33i  8251  axdc3lem4  8335  iscatd  13900  isfuncd  14064  isposd  14414  joinle  14452  pospropd  14563  imasmnd2  14734  grpinveu  14841  grpid  14842  imasgrp2  14935  dmdprdd  15562  pgpfac1lem5  15639  imasrng  15727  islmodd  15958  lmodvsghm  16007  islssd  16014  islmhm2  16116  psrbaglefi  16439  mulgghm2  16788  isphld  16887  riinopn  16983  ordtbaslem  17254  subbascn  17320  haust1  17418  isnrm2  17424  isnrm3  17425  lmmo  17446  nllyidm  17554  tx1stc  17684  filin  17888  filtop  17889  isfil2  17890  infil  17897  fgfil  17909  isufil2  17942  ufileu  17953  filufint  17954  flimopn  18009  flimrest  18017  isxmetd  18358  met2ndc  18555  icccmplem2  18856  lmmbr  19213  cfil3i  19224  equivcfil  19254  bcthlem5  19283  volfiniun  19443  dvidlem  19804  ulmdvlem3  20320  grporcan  21811  grpoinveu  21812  grpoid  21813  grpoasscan1  21827  cvxpcon  24931  cvxscon  24932  predpo  25461  ax5seg  25879  axcontlem4  25908  axcont  25917  broutsideof2  26058  nn0prpwlem  26327  fgmin  26401  cntotbnd  26507  heiborlem6  26527  heiborlem10  26531  rngonegmn1l  26567  rngonegmn1r  26568  rngoneglmul  26569  rngonegrmul  26570  crngm23  26614  prnc  26679  pridlc3  26685  dmncan1  26688  lsmsat  29868  eqlkr  29959  llncmp  30381  2at0mat0  30384  llncvrlpln  30417  lplncmp  30421  lplnexllnN  30423  lplncvrlvol  30475  lvolcmp  30476  linepsubN  30611  pmapsub  30627  paddasslem16  30694  pmodlem2  30706  lhp2lt  30860  ltrneq2  31007  cdlemf2  31421  cdlemk34  31769  cdlemn11pre  32070  dihord2pre  32085
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator