Theorem 3impa 1197

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  ex3  1198  3impdir  1307  syl3an9b  1323  biimp3a  1358  stoic3  1451  rspec3  2596  rspc3v  2893  raltpg  3686  rextpg  3687  disjiun  4039  otexg  4274  opelopabt  4308  tpexg  4491  3optocl  4753  fun2ssres  5314  funssfv  5602  fvun1  5645  foco2  5822  f1elima  5842  eloprabga  6032  caovimo  6140  ot1stg  6238  ot2ndg  6239  ot3rdgg  6240  brtposg  6340  rdgexggg  6463  rdgivallem  6467  nnmass  6573  nndir  6576  nnaword  6597  th3q  6727  ecovass  6731  ecoviass  6732  fpmg  6761  findcard  6985  unfiin  7023  addasspig  7443  mulasspig  7445  mulcanpig  7448  ltapig  7451  ltmpig  7452  addassnqg  7495  ltbtwnnqq  7528  mulnnnq0  7563  addassnq0  7575  genpassl  7637  genpassu  7638  genpassg  7639  aptiprleml  7752  adddir  8063  le2tri3i  8181  addsub12  8285  subdir  8458  reapmul1  8668  recexaplem2  8725  div12ap  8767  divdiv32ap  8793  divdivap1  8796  lble  9020  zaddcllemneg  9411  fnn0ind  9489  xrltso  9918  iccgelb  10054  elicc4  10062  elfz  10136  fzrevral  10227  expnegap0  10692  expgt0  10717  expge0  10720  expge1  10721  mulexpzap  10724  expp1zap  10733  expm1ap  10734  apexp1  10863  ccatsymb  11058  abssubap0  11401  binom  11795  dvds0lem  12112  dvdsnegb  12119  muldvds1  12127  muldvds2  12128  divalgmodcl  12239  gcd2n0cl  12290  lcmdvds  12401  prmdvdsexp  12470  rpexp1i  12476  eqglact  13561  lss0cl  14131  cnpval  14670  cnf2  14677  cnnei  14704  blssec  14910  blpnfctr  14911  mopni2  14955  mopni3  14956  dvply1  15237