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  7541  addasspig  7698  mulasspig  7700  mulcanpig  7703  ltapig  7706  ltmpig  7707  addassnqg  7750  ltbtwnnqq  7783  mulnnnq0  7818  addassnq0  7830  genpassl  7892  genpassu  7893  genpassg  7894  aptiprleml  8007  adddir  8318  le2tri3i  8436  addsub12  8541  subdir  8715  reapmul1  8926  recexaplem2  8983  div12ap  9027  divdiv32ap  9053  divdivap1  9056  lble  9280  zaddcllemneg  9688  fnn0ind  9767  xrltso  10209  iccgelb  10345  elicc4  10353  elfz  10428  fzrevral  10523  expnegap0  10999  expgt0  11024  expge0  11027  expge1  11028  mulexpzap  11031  expp1zap  11040  expm1ap  11041  apexp1  11172  ccatsymb  11386  abssubap0  11873  binom  12270  dvds0lem  12587  dvdsnegb  12594  muldvds1  12602  muldvds2  12603  divalgmodcl  12714  gcd2n0cl  12765  lcmdvds  12876  prmdvdsexp  12946  rpexp1i  12952  eqglact  14081  lss0cl  14790  cnpval  15390  cnf2  15397  cnnei  15424  blssec  15630  blpnfctr  15631  mopni2  15675  mopni3  15676  dvply1  15957  uhgrm  16485  upgrm  16507  upgr1or2  16508