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

Theorem 3exp2 1276
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 448 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1275 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3anassrs  1281  pm2.61da3ne  2867  po2nr  4959  predpo  5598  fliftfund  6438  frfi  8064  fin33i  9048  axdc3lem4  9132  relexpaddd  13585  iscatd  16100  isfuncd  16291  isposd  16721  pospropd  16900  imasmnd2  17093  grpinveu  17222  grpid  17223  grpasscan1  17244  imasgrp2  17296  dmdprdd  18164  pgpfac1lem5  18244  imasring  18385  islmodd  18635  lmodvsghm  18690  islssd  18700  islmhm2  18802  psrbaglefi  19136  mulgghm2  19606  isphld  19760  riinopn  20477  ordtbaslem  20741  subbascn  20807  haust1  20905  isnrm2  20911  isnrm3  20912  lmmo  20933  nllyidm  21041  tx1stc  21202  filin  21407  filtop  21408  isfil2  21409  infil  21416  fgfil  21428  isufil2  21461  ufileu  21472  filufint  21473  flimopn  21528  flimrest  21536  isxmetd  21879  met2ndc  22076  icccmplem2  22363  lmmbr  22779  cfil3i  22790  equivcfil  22820  bcthlem5  22847  volfiniun  23036  dvidlem  23399  ulmdvlem3  23874  ax5seg  25533  axcontlem4  25562  axcont  25571  grporcan  26519  grpoinveu  26520  grpoid  26521  cvxpcon  30281  cvxscon  30282  mclsax  30523  mclsppslem  30537  broutsideof2  31202  nn0prpwlem  31290  fgmin  31338  poimirlem27  32406  poimirlem29  32408  poimirlem31  32410  cntotbnd  32565  heiborlem6  32585  heiborlem10  32589  rngonegmn1l  32710  rngonegmn1r  32711  rngoneglmul  32712  rngonegrmul  32713  crngm23  32771  prnc  32836  pridlc3  32842  dmncan1  32845  lsmsat  33113  eqlkr  33204  llncmp  33626  2at0mat0  33629  llncvrlpln  33662  lplncmp  33666  lplnexllnN  33668  lplncvrlvol  33720  lvolcmp  33721  linepsubN  33856  pmapsub  33872  paddasslem16  33939  pmodlem2  33951  lhp2lt  34105  ltrneq2  34252  cdlemf2  34668  cdlemk34  35016  cdlemn11pre  35317  dihord2pre  35332
  Copyright terms: Public domain W3C validator