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

Theorem 3imp 1098
 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 887 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 243 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 114 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  3impa  1099  3impb  1100  3impia  1101  3impib  1102  3com23  1110  3an1rs  1116  3imp1  1117  3impd  1118  syl3an2  1169  syl3an3  1170  3jao  1196  biimp3ar  1236  poxp  5853  tfrlemibxssdm  5941  nndi  6065  nnmass  6066  difelfzle  8992  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  elfzodifsumelfzo  9057  mulexp  9294  expadd  9297  expmul  9300  bernneq  9369
 Copyright terms: Public domain W3C validator