Theorem 3impa 1196

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

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

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 982

This theorem is referenced by:  ex3  1197  3impdir  1305  syl3an9b  1321  biimp3a  1356  stoic3  1442  rspec3  2587  rspc3v  2884  raltpg  3676  rextpg  3677  disjiun  4029  otexg  4264  opelopabt  4297  tpexg  4480  3optocl  4742  fun2ssres  5302  funssfv  5585  fvun1  5628  foco2  5801  f1elima  5821  eloprabga  6010  caovimo  6118  ot1stg  6211  ot2ndg  6212  ot3rdgg  6213  brtposg  6313  rdgexggg  6436  rdgivallem  6440  nnmass  6546  nndir  6549  nnaword  6570  th3q  6700  ecovass  6704  ecoviass  6705  fpmg  6734  findcard  6950  unfiin  6988  addasspig  7399  mulasspig  7401  mulcanpig  7404  ltapig  7407  ltmpig  7408  addassnqg  7451  ltbtwnnqq  7484  mulnnnq0  7519  addassnq0  7531  genpassl  7593  genpassu  7594  genpassg  7595  aptiprleml  7708  adddir  8019  le2tri3i  8137  addsub12  8241  subdir  8414  reapmul1  8624  recexaplem2  8681  div12ap  8723  divdiv32ap  8749  divdivap1  8752  lble  8976  zaddcllemneg  9367  fnn0ind  9444  xrltso  9873  iccgelb  10009  elicc4  10017  elfz  10091  fzrevral  10182  expnegap0  10641  expgt0  10666  expge0  10669  expge1  10670  mulexpzap  10673  expp1zap  10682  expm1ap  10683  apexp1  10812  abssubap0  11257  binom  11651  dvds0lem  11968  dvdsnegb  11975  muldvds1  11983  muldvds2  11984  divalgmodcl  12095  gcd2n0cl  12146  lcmdvds  12257  prmdvdsexp  12326  rpexp1i  12332  eqglact  13365  lss0cl  13935  cnpval  14444  cnf2  14451  cnnei  14478  blssec  14684  blpnfctr  14685  mopni2  14729  mopni3  14730  dvply1  15011