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

Theorem 3imp 1188
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 975 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 254 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 120 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  3impa  1189  3imp31  1191  3imp231  1192  3impb  1194  3impia  1195  3impib  1196  3com23  1204  3an1rs  1214  3imp1  1215  3impd  1216  syl3an2  1267  syl3an3  1268  3jao  1296  biimp3ar  1341  poxp  6211  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  nndi  6465  nnmass  6466  pr2nelem  7168  xnn0lenn0nn0  9822  difelfzle  10090  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  mulexp  10515  expadd  10518  expmul  10521  bernneq  10596  facdiv  10672  addmodlteqALT  11819  ltoddhalfle  11852  halfleoddlt  11853  dfgcd2  11969  cncongr1  12057  oddprmgt2  12088  prmfac1  12106  infpnlem1  12311  fiinopn  12796  opnneissb  12949  blssps  13221  blss  13222  2sqlem10  13755
  Copyright terms: Public domain W3C validator