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

Theorem 3exp2 1456
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 399 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1455 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3anassrs  1462  pm2.61da3ne  3078  po2nr  5258  predpo  5925  fliftfund  6797  frfi  8454  fin33i  9486  axdc3lem4  9570  relexpaddd  14037  iscatd  16558  isfuncd  16749  isposd  17180  pospropd  17359  imasmnd2  17552  grpinveu  17681  grpid  17682  grpasscan1  17703  imasgrp2  17755  dmdprdd  18620  pgpfac1lem5  18700  imasring  18841  islmodd  19093  lmodvsghm  19148  islssd  19160  islmhm2  19265  psrbaglefi  19601  mulgghm2  20073  isphld  20229  riinopn  20947  ordtbaslem  21227  subbascn  21293  haust1  21391  isnrm2  21397  isnrm3  21398  lmmo  21419  nllyidm  21527  tx1stc  21688  filin  21892  filtop  21893  isfil2  21894  infil  21901  fgfil  21913  isufil2  21946  ufileu  21957  filufint  21958  flimopn  22013  flimrest  22021  isxmetd  22365  met2ndc  22562  icccmplem2  22860  lmmbr  23290  cfil3i  23301  equivcfil  23331  bcthlem5  23359  volfiniun  23551  dvidlem  23916  ulmdvlem3  24393  ax5seg  26055  axcontlem4  26084  axcont  26093  grporcan  27724  grpoinveu  27725  grpoid  27726  cvxpconn  31569  cvxsconn  31570  mclsax  31811  mclsppslem  31825  broutsideof2  32572  nn0prpwlem  32660  fgmin  32708  poimirlem27  33768  poimirlem29  33770  poimirlem31  33772  cntotbnd  33925  heiborlem6  33945  heiborlem10  33949  rngonegmn1l  34070  rngonegmn1r  34071  rngoneglmul  34072  rngonegrmul  34073  crngm23  34131  prnc  34196  pridlc3  34202  dmncan1  34205  lsmsat  34807  eqlkr  34898  llncmp  35321  2at0mat0  35324  llncvrlpln  35357  lplncmp  35361  lplnexllnN  35363  lplncvrlvol  35415  lvolcmp  35416  linepsubN  35551  pmapsub  35567  paddasslem16  35634  pmodlem2  35646  lhp2lt  35800  ltrneq2  35947  cdlemf2  36361  cdlemk34  36709  cdlemn11pre  37009  dihord2pre  37024
  Copyright terms: Public domain W3C validator