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

Theorem 3exp2 1282
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
3exp2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
21ex 450 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1281 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  3anassrs  1287  pm2.61da3ne  2879  po2nr  5018  predpo  5667  fliftfund  6528  frfi  8165  fin33i  9151  axdc3lem4  9235  relexpaddd  13744  iscatd  16274  isfuncd  16465  isposd  16895  pospropd  17074  imasmnd2  17267  grpinveu  17396  grpid  17397  grpasscan1  17418  imasgrp2  17470  dmdprdd  18338  pgpfac1lem5  18418  imasring  18559  islmodd  18809  lmodvsghm  18864  islssd  18876  islmhm2  18978  psrbaglefi  19312  mulgghm2  19785  isphld  19939  riinopn  20653  ordtbaslem  20932  subbascn  20998  haust1  21096  isnrm2  21102  isnrm3  21103  lmmo  21124  nllyidm  21232  tx1stc  21393  filin  21598  filtop  21599  isfil2  21600  infil  21607  fgfil  21619  isufil2  21652  ufileu  21663  filufint  21664  flimopn  21719  flimrest  21727  isxmetd  22071  met2ndc  22268  icccmplem2  22566  lmmbr  22996  cfil3i  23007  equivcfil  23037  bcthlem5  23065  volfiniun  23255  dvidlem  23619  ulmdvlem3  24094  ax5seg  25752  axcontlem4  25781  axcont  25790  grporcan  27260  grpoinveu  27261  grpoid  27262  cvxpconn  30985  cvxsconn  30986  mclsax  31227  mclsppslem  31241  broutsideof2  31924  nn0prpwlem  32012  fgmin  32060  poimirlem27  33107  poimirlem29  33109  poimirlem31  33111  cntotbnd  33266  heiborlem6  33286  heiborlem10  33290  rngonegmn1l  33411  rngonegmn1r  33412  rngoneglmul  33413  rngonegrmul  33414  crngm23  33472  prnc  33537  pridlc3  33543  dmncan1  33546  lsmsat  33814  eqlkr  33905  llncmp  34327  2at0mat0  34330  llncvrlpln  34363  lplncmp  34367  lplnexllnN  34369  lplncvrlvol  34421  lvolcmp  34422  linepsubN  34557  pmapsub  34573  paddasslem16  34640  pmodlem2  34652  lhp2lt  34806  ltrneq2  34953  cdlemf2  35369  cdlemk34  35717  cdlemn11pre  36018  dihord2pre  36033
  Copyright terms: Public domain W3C validator