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

Theorem 3imp 1156
 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 945 . 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 943 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106 This theorem depends on definitions:  df-bi 116  df-3an 945 This theorem is referenced by:  3impa  1157  3impb  1158  3impia  1159  3impib  1160  3com23  1168  3an1rs  1178  3imp1  1179  3impd  1180  syl3an2  1231  syl3an3  1232  3jao  1260  biimp3ar  1305  poxp  6081  tfrlemibxssdm  6176  tfr1onlembxssdm  6192  tfrcllembxssdm  6205  nndi  6334  nnmass  6335  pr2nelem  6994  xnn0lenn0nn0  9535  difelfzle  9798  fzo1fzo0n0  9847  elfzo0z  9848  fzofzim  9852  elfzodifsumelfzo  9865  mulexp  10219  expadd  10222  expmul  10225  bernneq  10299  facdiv  10371  addmodlteqALT  11399  ltoddhalfle  11432  halfleoddlt  11433  dfgcd2  11542  cncongr1  11624  oddprmgt2  11654  prmfac1  11670  fiinopn  12008  opnneissb  12161  blssps  12410  blss  12411
 Copyright terms: Public domain W3C validator