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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ex3  1226  3impdir  1335  syl3an9b  1351  biimp3a  1386  stoic3  1480  rspec3  2640  rspc3v  2946  raltpg  3762  rextpg  3763  disjiun  4125  otexg  4370  opelopabt  4404  tpexg  4590  3optocl  4853  fun2ssres  5421  funssfv  5721  fvun1  5769  foco2  5959  f1elima  5979  eloprabga  6175  caovimo  6283  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  brtposg  6525  rdgexggg  6648  rdgivallem  6652  nnmass  6760  nndir  6763  nnaword  6784  th3q  6914  ecovass  6918  ecoviass  6919  fpmg  6955  findcard  7192  unfiin  7233  pr1or2  7540  addasspig  7697  mulasspig  7699  mulcanpig  7702  ltapig  7705  ltmpig  7706  addassnqg  7749  ltbtwnnqq  7782  mulnnnq0  7817  addassnq0  7829  genpassl  7891  genpassu  7892  genpassg  7893  aptiprleml  8006  adddir  8317  le2tri3i  8434  addsub12  8539  subdir  8713  reapmul1  8923  recexaplem2  8980  div12ap  9024  divdiv32ap  9050  divdivap1  9053  lble  9277  zaddcllemneg  9683  fnn0ind  9762  xrltso  10198  iccgelb  10334  elicc4  10342  elfz  10417  fzrevral  10512  expnegap0  10984  expgt0  11009  expge0  11012  expge1  11013  mulexpzap  11016  expp1zap  11025  expm1ap  11026  apexp1  11156  ccatsymb  11370  abssubap0  11856  binom  12251  dvds0lem  12568  dvdsnegb  12575  muldvds1  12583  muldvds2  12584  divalgmodcl  12695  gcd2n0cl  12746  lcmdvds  12857  prmdvdsexp  12926  rpexp1i  12932  eqglact  14028  lss0cl  14706  cnpval  15299  cnf2  15306  cnnei  15333  blssec  15539  blpnfctr  15540  mopni2  15584  mopni3  15585  dvply1  15866  uhgrm  16319  upgrm  16341  upgr1or2  16342