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

Theorem 3imp 1176
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 965 . 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 963
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 965
This theorem is referenced by:  3impa  1177  3imp31  1178  3imp231  1179  3impb  1181  3impia  1182  3impib  1183  3com23  1191  3an1rs  1201  3imp1  1202  3impd  1203  syl3an2  1254  syl3an3  1255  3jao  1283  biimp3ar  1328  poxp  6180  tfrlemibxssdm  6275  tfr1onlembxssdm  6291  tfrcllembxssdm  6304  nndi  6434  nnmass  6435  pr2nelem  7127  xnn0lenn0nn0  9770  difelfzle  10037  fzo1fzo0n0  10086  elfzo0z  10087  fzofzim  10091  elfzodifsumelfzo  10104  mulexp  10462  expadd  10465  expmul  10468  bernneq  10542  facdiv  10616  addmodlteqALT  11755  ltoddhalfle  11788  halfleoddlt  11789  dfgcd2  11902  cncongr1  11984  oddprmgt2  12015  prmfac1  12031  fiinopn  12444  opnneissb  12597  blssps  12869  blss  12870
  Copyright terms: Public domain W3C validator