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

Theorem 3exp2 1346
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 413 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1345 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3anassrs  1352  pm2.61da3ne  3103  po2nr  5480  predpo  6159  fliftfund  7055  frfi  8751  fin33i  9779  axdc3lem4  9863  relexpaddd  14401  iscatd  16932  isfuncd  17123  isposd  17553  pospropd  17732  imasmnd2  17936  grpinveu  18076  grpid  18077  grpasscan1  18100  imasgrp2  18152  dmdprdd  19050  pgpfac1lem5  19130  imasring  19298  islmodd  19569  lmodvsghm  19624  islssd  19636  islmhm2  19739  psrbaglefi  20080  mulgghm2  20572  isphld  20726  riinopn  21444  ordtbaslem  21724  subbascn  21790  haust1  21888  isnrm2  21894  isnrm3  21895  lmmo  21916  nllyidm  22025  tx1stc  22186  filin  22390  filtop  22391  isfil2  22392  infil  22399  fgfil  22411  isufil2  22444  ufileu  22455  filufint  22456  flimopn  22511  flimrest  22519  isxmetd  22863  met2ndc  23060  icccmplem2  23358  lmmbr  23788  cfil3i  23799  equivcfil  23829  bcthlem5  23858  volfiniun  24075  dvidlem  24440  ulmdvlem3  24917  ax5seg  26651  axcontlem4  26680  axcont  26689  grporcan  28222  grpoinveu  28223  grpoid  28224  cvxpconn  32386  cvxsconn  32387  mclsax  32713  mclsppslem  32727  broutsideof2  33480  nn0prpwlem  33567  fgmin  33615  poimirlem27  34800  poimirlem29  34802  poimirlem31  34804  cntotbnd  34955  heiborlem6  34975  heiborlem10  34979  rngonegmn1l  35100  rngonegmn1r  35101  rngoneglmul  35102  rngonegrmul  35103  crngm23  35161  prnc  35226  pridlc3  35232  dmncan1  35235  lsmsat  36024  eqlkr  36115  llncmp  36538  2at0mat0  36541  llncvrlpln  36574  lplncmp  36578  lplnexllnN  36580  lplncvrlvol  36632  lvolcmp  36633  linepsubN  36768  pmapsub  36784  paddasslem16  36851  pmodlem2  36863  lhp2lt  37017  ltrneq2  37164  cdlemf2  37578  cdlemk34  37926  cdlemn11pre  38226  dihord2pre  38241
  Copyright terms: Public domain W3C validator