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

Theorem 3impa 1138
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3impa ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 356 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1137 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  3impdir  1230  syl3an9b  1246  biimp3a  1281  stoic3  1365  rspec3  2463  rspc3v  2736  raltpg  3490  rextpg  3491  disjiun  3832  otexg  4048  opelopabt  4080  tpexg  4260  3optocl  4504  fun2ssres  5043  funssfv  5314  fvun1  5354  foco2  5515  f1elima  5534  eloprabga  5717  caovimo  5820  ot1stg  5905  ot2ndg  5906  ot3rdgg  5907  brtposg  6001  rdgexggg  6124  rdgivallem  6128  nnmass  6230  nndir  6233  nnaword  6250  th3q  6377  ecovass  6381  ecoviass  6382  fpmg  6411  findcard  6584  unfiin  6616  addasspig  6868  mulasspig  6870  mulcanpig  6873  ltapig  6876  ltmpig  6877  addassnqg  6920  ltbtwnnqq  6953  mulnnnq0  6988  addassnq0  7000  genpassl  7062  genpassu  7063  genpassg  7064  aptiprleml  7177  adddir  7458  le2tri3i  7572  addsub12  7674  subdir  7843  reapmul1  8048  recexaplem2  8095  div12ap  8135  divdiv32ap  8161  divdivap1  8164  lble  8380  zaddcllemneg  8759  fnn0ind  8832  xrltso  9235  iccgelb  9319  elicc4  9327  elfz  9399  fzrevral  9486  expnegap0  9927  expgt0  9952  expge0  9955  expge1  9956  mulexpzap  9959  expp1zap  9968  expm1ap  9969  abssubap0  10487  binom  10838  dvds0lem  10886  dvdsnegb  10893  muldvds1  10901  muldvds2  10902  divalgmodcl  11008  gcd2n0cl  11041  lcmdvds  11141  prmdvdsexp  11207  rpexp1i  11213
  Copyright terms: Public domain W3C validator