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

Theorem 3imp 1107
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 896 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 247 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 118 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  3impa  1108  3impb  1109  3impia  1110  3impib  1111  3com23  1119  3an1rs  1125  3imp1  1126  3impd  1127  syl3an2  1178  syl3an3  1179  3jao  1205  biimp3ar  1250  poxp  5878  tfrlemibxssdm  5969  nndi  6093  nnmass  6094  difelfzle  9064  fzo1fzo0n0  9111  elfzo0z  9112  fzofzim  9116  elfzodifsumelfzo  9129  mulexp  9424  expadd  9427  expmul  9430  bernneq  9501  facdiv  9570  addmodlteqALT  10134  ltoddhalfle  10168  halfleoddlt  10169
  Copyright terms: Public domain W3C validator