Theorem 3impa 1221

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

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

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 1007

This theorem is referenced by:  ex3  1222  3impdir  1331  syl3an9b  1347  biimp3a  1382  stoic3  1476  rspec3  2634  rspc3v  2940  raltpg  3747  rextpg  3748  disjiun  4109  otexg  4351  opelopabt  4385  tpexg  4570  3optocl  4833  fun2ssres  5401  funssfv  5701  fvun1  5748  foco2  5932  f1elima  5952  eloprabga  6148  caovimo  6256  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  brtposg  6498  rdgexggg  6621  rdgivallem  6625  nnmass  6733  nndir  6736  nnaword  6757  th3q  6887  ecovass  6891  ecoviass  6892  fpmg  6921  findcard  7158  unfiin  7199  pr1or2  7504  addasspig  7661  mulasspig  7663  mulcanpig  7666  ltapig  7669  ltmpig  7670  addassnqg  7713  ltbtwnnqq  7746  mulnnnq0  7781  addassnq0  7793  genpassl  7855  genpassu  7856  genpassg  7857  aptiprleml  7970  adddir  8281  le2tri3i  8398  addsub12  8503  subdir  8677  reapmul1  8887  recexaplem2  8944  div12ap  8988  divdiv32ap  9014  divdivap1  9017  lble  9241  zaddcllemneg  9636  fnn0ind  9715  xrltso  10151  iccgelb  10287  elicc4  10295  elfz  10370  fzrevral  10464  expnegap0  10936  expgt0  10961  expge0  10964  expge1  10965  mulexpzap  10968  expp1zap  10977  expm1ap  10978  apexp1  11108  ccatsymb  11318  abssubap0  11803  binom  12198  dvds0lem  12515  dvdsnegb  12522  muldvds1  12530  muldvds2  12531  divalgmodcl  12642  gcd2n0cl  12693  lcmdvds  12804  prmdvdsexp  12873  rpexp1i  12879  eqglact  13981  lss0cl  14646  cnpval  15192  cnf2  15199  cnnei  15226  blssec  15432  blpnfctr  15433  mopni2  15477  mopni3  15478  dvply1  15759  uhgrm  16202  upgrm  16224  upgr1or2  16225