Theorem 3impa 1159

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

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

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

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

This theorem is referenced by:  3impdir  1255  syl3an9b  1271  biimp3a  1306  stoic3  1390  rspec3  2496  rspc3v  2775  raltpg  3542  rextpg  3543  disjiun  3890  otexg  4112  opelopabt  4144  tpexg  4325  3optocl  4577  fun2ssres  5124  funssfv  5401  fvun1  5441  foco2  5609  f1elima  5628  eloprabga  5812  caovimo  5918  ot1stg  6004  ot2ndg  6005  ot3rdgg  6006  brtposg  6105  rdgexggg  6228  rdgivallem  6232  nnmass  6337  nndir  6340  nnaword  6361  th3q  6488  ecovass  6492  ecoviass  6493  fpmg  6522  findcard  6735  unfiin  6767  addasspig  7086  mulasspig  7088  mulcanpig  7091  ltapig  7094  ltmpig  7095  addassnqg  7138  ltbtwnnqq  7171  mulnnnq0  7206  addassnq0  7218  genpassl  7280  genpassu  7281  genpassg  7282  aptiprleml  7395  adddir  7681  le2tri3i  7795  addsub12  7898  subdir  8067  reapmul1  8275  recexaplem2  8326  div12ap  8367  divdiv32ap  8393  divdivap1  8396  lble  8615  zaddcllemneg  8997  fnn0ind  9071  xrltso  9475  iccgelb  9608  elicc4  9616  elfz  9689  fzrevral  9778  expnegap0  10194  expgt0  10219  expge0  10222  expge1  10223  mulexpzap  10226  expp1zap  10235  expm1ap  10236  abssubap0  10754  binom  11145  dvds0lem  11351  dvdsnegb  11358  muldvds1  11366  muldvds2  11367  divalgmodcl  11473  gcd2n0cl  11506  lcmdvds  11606  prmdvdsexp  11672  rpexp1i  11678  cnpval  12209  cnf2  12216  cnnei  12243  blssec  12427  blpnfctr  12428  mopni2  12472  mopni3  12473