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

Theorem 3imp2 1346
 Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
3imp2 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)

Proof of Theorem 3imp2
StepHypRef Expression
1 3imp1.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
213impd 1345 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 410 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  wereu  5515  ovg  7294  fisup2g  8918  fiinf2g  8950  cfcoflem  9685  ttukeylem5  9926  dedekindle  10795  grplcan  18156  mulgnnass  18257  dmdprdsplit2  19164  mulgass2  19350  lmodvsdi  19653  lmodvsdir  19654  lmodvsass  19655  lss1d  19731  islmhm2  19806  lspsolvlem  19910  lbsextlem2  19927  cygznlem2a  20263  isphld  20347  t0dist  21937  hausnei  21940  nrmsep3  21967  fclsopni  22627  fcfneii  22649  ax5seglem5  26734  axcont  26777  grporcan  28308  grpolcan  28320  slmdvsdi  30900  slmdvsdir  30901  slmdvsass  30902  elrspunidl  31021  zarcmplem  31246  mclsppslem  32955  broutsideof2  33708  poimirlem31  35104  broucube  35107  frinfm  35189  crngm23  35456  pridl  35491  pridlc  35525  dmnnzd  35529  dmncan1  35530  paddasslem5  37136  or2expropbi  43641  elsetpreimafveqfv  43924  sfprmdvdsmersenne  44136
 Copyright terms: Public domain W3C validator