Theorem 3impa 1177

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 362	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1176	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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  ax-ia3 107

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

This theorem is referenced by:  3impdir  1273  syl3an9b  1289  biimp3a  1324  stoic3  1408  rspec3  2544  rspc3v  2829  raltpg  3608  rextpg  3609  disjiun  3956  otexg  4185  opelopabt  4217  tpexg  4398  3optocl  4657  fun2ssres  5206  funssfv  5487  fvun1  5527  foco2  5695  f1elima  5714  eloprabga  5898  caovimo  6004  ot1stg  6090  ot2ndg  6091  ot3rdgg  6092  brtposg  6191  rdgexggg  6314  rdgivallem  6318  nnmass  6423  nndir  6426  nnaword  6447  th3q  6574  ecovass  6578  ecoviass  6579  fpmg  6608  findcard  6822  unfiin  6859  addasspig  7229  mulasspig  7231  mulcanpig  7234  ltapig  7237  ltmpig  7238  addassnqg  7281  ltbtwnnqq  7314  mulnnnq0  7349  addassnq0  7361  genpassl  7423  genpassu  7424  genpassg  7425  aptiprleml  7538  adddir  7848  le2tri3i  7964  addsub12  8067  subdir  8240  reapmul1  8449  recexaplem2  8505  div12ap  8546  divdiv32ap  8572  divdivap1  8575  lble  8797  zaddcllemneg  9185  fnn0ind  9259  xrltso  9681  iccgelb  9814  elicc4  9822  elfz  9896  fzrevral  9985  expnegap0  10405  expgt0  10430  expge0  10433  expge1  10434  mulexpzap  10437  expp1zap  10446  expm1ap  10447  apexp1  10569  abssubap0  10967  binom  11358  dvds0lem  11670  dvdsnegb  11677  muldvds1  11685  muldvds2  11686  divalgmodcl  11792  gcd2n0cl  11825  lcmdvds  11928  prmdvdsexp  11994  rpexp1i  12000  cnpval  12545  cnf2  12552  cnnei  12579  blssec  12785  blpnfctr  12786  mopni2  12830  mopni3  12831