ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3imp GIF version

Theorem 3imp 1135
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
3imp ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 924 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 252 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 119 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  3impa  1136  3impb  1137  3impia  1138  3impib  1139  3com23  1147  3an1rs  1153  3imp1  1154  3impd  1155  syl3an2  1206  syl3an3  1207  3jao  1235  biimp3ar  1280  poxp  5954  tfrlemibxssdm  6046  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  nndi  6201  nnmass  6202  pr2nelem  6763  difelfzle  9473  fzo1fzo0n0  9522  elfzo0z  9523  fzofzim  9527  elfzodifsumelfzo  9540  mulexp  9892  expadd  9895  expmul  9898  bernneq  9970  facdiv  10042  addmodlteqALT  10735  ltoddhalfle  10768  halfleoddlt  10769  dfgcd2  10878  cncongr1  10960  oddprmgt2  10990  prmfac1  11006
  Copyright terms: Public domain W3C validator