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

Theorem 3imp1 1271
Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3imp1.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
3imp1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3imp1
StepHypRef Expression
1 3imp1.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
213imp 1248 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
32imp 443 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:  reupick2  3871  indcardi  8725  ledivge1le  11736  expcan  12733  ltexp2  12734  leexp1a  12739  expnbnd  12813  cshf1  13356  rtrclreclem4  13598  relexpindlem  13600  ncoprmlnprm  15223  xrsdsreclblem  19560  matecl  19998  scmateALT  20085  riinopn  20486  neindisj2  20685  filufint  21482  tsmsxp  21716  spthonepeq  25911  usg2wlkeq  26030  rusgraprop4  26265  vdn0frgrav2  26344  vdn1frgrav2  26346  usgreghash2spot  26390  homco1  27878  homulass  27879  hoadddir  27881  mblfinlem3  32442  zerdivemp1x  32740  athgt  33584  psubspi  33875  paddasslem14  33961  iccpartigtl  39786  lighneal  39891  eluzge0nn0  40197  ewlkle  40829  uspgr2wlkeq  40876  spthonepeq-av  40980  wwlksm1edg  41100  clwwisshclwws  41257  3vfriswmgr  41470  av-extwwlkfablem2  41532
  Copyright terms: Public domain W3C validator