Theorem 3impa 1176

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

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 361	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1175	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3impdir  1272  syl3an9b  1288  biimp3a  1323  stoic3  1407  rspec3  2522  rspc3v  2805  raltpg  3576  rextpg  3577  disjiun  3924  otexg  4152  opelopabt  4184  tpexg  4365  3optocl  4617  fun2ssres  5166  funssfv  5447  fvun1  5487  foco2  5655  f1elima  5674  eloprabga  5858  caovimo  5964  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  brtposg  6151  rdgexggg  6274  rdgivallem  6278  nnmass  6383  nndir  6386  nnaword  6407  th3q  6534  ecovass  6538  ecoviass  6539  fpmg  6568  findcard  6782  unfiin  6814  addasspig  7138  mulasspig  7140  mulcanpig  7143  ltapig  7146  ltmpig  7147  addassnqg  7190  ltbtwnnqq  7223  mulnnnq0  7258  addassnq0  7270  genpassl  7332  genpassu  7333  genpassg  7334  aptiprleml  7447  adddir  7757  le2tri3i  7872  addsub12  7975  subdir  8148  reapmul1  8357  recexaplem2  8413  div12ap  8454  divdiv32ap  8480  divdivap1  8483  lble  8705  zaddcllemneg  9093  fnn0ind  9167  xrltso  9582  iccgelb  9715  elicc4  9723  elfz  9796  fzrevral  9885  expnegap0  10301  expgt0  10326  expge0  10329  expge1  10330  mulexpzap  10333  expp1zap  10342  expm1ap  10343  abssubap0  10862  binom  11253  dvds0lem  11503  dvdsnegb  11510  muldvds1  11518  muldvds2  11519  divalgmodcl  11625  gcd2n0cl  11658  lcmdvds  11760  prmdvdsexp  11826  rpexp1i  11832  cnpval  12367  cnf2  12374  cnnei  12401  blssec  12607  blpnfctr  12608  mopni2  12652  mopni3  12653