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

Theorem 3impa 1134
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 1133 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
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 922
This theorem is referenced by:  3impdir  1226  syl3an9b  1242  biimp3a  1277  stoic3  1361  rspec3  2452  rspc3v  2717  raltpg  3453  rextpg  3454  otexg  3993  opelopabt  4025  tpexg  4205  3optocl  4444  fun2ssres  4973  funssfv  5231  fvun1  5271  foco2  5350  f1elima  5444  eloprabga  5622  caovimo  5725  ot1stg  5810  ot2ndg  5811  ot3rdgg  5812  brtposg  5903  rdgexggg  6026  rdgivallem  6030  nnmass  6131  nndir  6134  nnaword  6150  th3q  6277  ecovass  6281  ecoviass  6282  findcard  6422  unfiin  6444  addasspig  6582  mulasspig  6584  mulcanpig  6587  ltapig  6590  ltmpig  6591  addassnqg  6634  ltbtwnnqq  6667  mulnnnq0  6702  addassnq0  6714  genpassl  6776  genpassu  6777  genpassg  6778  aptiprleml  6891  adddir  7172  le2tri3i  7286  addsub12  7388  subdir  7557  reapmul1  7762  recexaplem2  7809  div12ap  7849  divdiv32ap  7875  divdivap1  7878  lble  8092  zaddcllemneg  8471  fnn0ind  8544  xrltso  8947  iccgelb  9031  elicc4  9039  elfz  9111  fzrevral  9198  expivallem  9574  expnegap0  9581  expgt0  9606  expge0  9609  expge1  9610  mulexpzap  9613  expp1zap  9622  expm1ap  9623  abssubap0  10114  dvds0lem  10350  dvdsnegb  10357  muldvds1  10365  muldvds2  10366  divalgmodcl  10472  gcd2n0cl  10505  lcmdvds  10605  prmdvdsexp  10671  rpexp1i  10677
  Copyright terms: Public domain W3C validator