Theorem 3impa 1225

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 1224	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1011

This theorem is referenced by:  ex3  1226  3impdir  1335  syl3an9b  1351  biimp3a  1386  stoic3  1480  rspec3  2640  rspc3v  2946  raltpg  3758  rextpg  3759  disjiun  4120  otexg  4365  opelopabt  4399  tpexg  4585  3optocl  4848  fun2ssres  5416  funssfv  5716  fvun1  5763  foco2  5949  f1elima  5969  eloprabga  6165  caovimo  6273  ot1stg  6376  ot2ndg  6377  ot3rdgg  6378  brtposg  6515  rdgexggg  6638  rdgivallem  6642  nnmass  6750  nndir  6753  nnaword  6774  th3q  6904  ecovass  6908  ecoviass  6909  fpmg  6945  findcard  7182  unfiin  7223  pr1or2  7530  addasspig  7687  mulasspig  7689  mulcanpig  7692  ltapig  7695  ltmpig  7696  addassnqg  7739  ltbtwnnqq  7772  mulnnnq0  7807  addassnq0  7819  genpassl  7881  genpassu  7882  genpassg  7883  aptiprleml  7996  adddir  8307  le2tri3i  8424  addsub12  8529  subdir  8703  reapmul1  8913  recexaplem2  8970  div12ap  9014  divdiv32ap  9040  divdivap1  9043  lble  9267  zaddcllemneg  9662  fnn0ind  9741  xrltso  10177  iccgelb  10313  elicc4  10321  elfz  10396  fzrevral  10490  expnegap0  10962  expgt0  10987  expge0  10990  expge1  10991  mulexpzap  10994  expp1zap  11003  expm1ap  11004  apexp1  11134  ccatsymb  11348  abssubap0  11834  binom  12229  dvds0lem  12546  dvdsnegb  12553  muldvds1  12561  muldvds2  12562  divalgmodcl  12673  gcd2n0cl  12724  lcmdvds  12835  prmdvdsexp  12904  rpexp1i  12910  eqglact  14005  lss0cl  14678  cnpval  15222  cnf2  15229  cnnei  15256  blssec  15462  blpnfctr  15463  mopni2  15507  mopni3  15508  dvply1  15789  uhgrm  16233  upgrm  16255  upgr1or2  16256