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

Theorem 3imp2 1458
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 1457 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 395 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 1109
This theorem is referenced by:  wereu  5275  ovg  6999  fisup2g  8583  fiinf2g  8615  cfcoflem  9349  ttukeylem5  9590  dedekindle  10457  grplcan  17747  mulgnnass  17844  dmdprdsplit2  18715  mulgass2  18871  lmodvsdi  19158  lmodvsdir  19159  lmodvsass  19160  lss1d  19238  islmhm2  19313  lspsolvlem  19418  lbsextlem2  19436  cygznlem2a  20191  isphld  20277  t0dist  21412  hausnei  21415  nrmsep3  21442  fclsopni  22101  fcfneii  22123  ax5seglem5  26107  axcont  26150  grporcan  27832  grpolcan  27844  slmdvsdi  30218  slmdvsdir  30219  slmdvsass  30220  mclsppslem  31931  broutsideof2  32676  poimirlem31  33867  broucube  33870  frinfm  33956  crngm23  34226  pridl  34261  pridlc  34295  dmnnzd  34299  dmncan1  34300  paddasslem5  35783  sfprmdvdsmersenne  42199
  Copyright terms: Public domain W3C validator