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

Theorem 3impa 1099
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 346 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1098 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  3impdir  1191  syl3an9b  1205  biimp3a  1235  stoic3  1320  rspec3  2409  rspc3v  2665  raltpg  3423  rextpg  3424  otexg  3967  opelopabt  3999  tpexg  4179  3optocl  4418  fun2ssres  4943  funssfv  5199  fvun1  5239  foco2  5318  f1elima  5412  eloprabga  5591  caovimo  5694  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  brtposg  5869  rdgexggg  5964  rdgivallem  5968  frecsuclem1  5987  nnmass  6066  nndir  6069  nnaword  6084  th3q  6211  ecovass  6215  ecoviass  6216  findcard  6345  addasspig  6426  mulasspig  6428  mulcanpig  6431  ltapig  6434  ltmpig  6435  addassnqg  6478  ltbtwnnqq  6511  mulnnnq0  6546  addassnq0  6558  genpassl  6620  genpassu  6621  genpassg  6622  aptiprleml  6735  adddir  7016  le2tri3i  7124  addsub12  7222  subdir  7381  reapmul1  7584  recexaplem2  7631  div12ap  7671  divdiv32ap  7694  divdivap1  7697  zaddcllemneg  8282  fnn0ind  8352  xrltso  8715  iccgelb  8799  elicc4  8807  elfz  8878  fzrevral  8965  expivallem  9230  expnegap0  9237  expgt0  9262  expge0  9265  expge1  9266  mulexpzap  9269  expp1zap  9277  expm1ap  9278  abssubap0  9660
  Copyright terms: Public domain W3C validator