Theorem 3impa 1220

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

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

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 1006

This theorem is referenced by:  ex3  1221  3impdir  1330  syl3an9b  1346  biimp3a  1381  stoic3  1475  rspec3  2622  rspc3v  2926  raltpg  3722  rextpg  3723  disjiun  4083  otexg  4322  opelopabt  4356  tpexg  4541  3optocl  4804  fun2ssres  5370  funssfv  5665  fvun1  5712  foco2  5893  f1elima  5913  eloprabga  6107  caovimo  6215  ot1stg  6314  ot2ndg  6315  ot3rdgg  6316  brtposg  6419  rdgexggg  6542  rdgivallem  6546  nnmass  6654  nndir  6657  nnaword  6678  th3q  6808  ecovass  6812  ecoviass  6813  fpmg  6842  findcard  7076  unfiin  7117  pr1or2  7398  addasspig  7549  mulasspig  7551  mulcanpig  7554  ltapig  7557  ltmpig  7558  addassnqg  7601  ltbtwnnqq  7634  mulnnnq0  7669  addassnq0  7681  genpassl  7743  genpassu  7744  genpassg  7745  aptiprleml  7858  adddir  8169  le2tri3i  8287  addsub12  8391  subdir  8564  reapmul1  8774  recexaplem2  8831  div12ap  8873  divdiv32ap  8899  divdivap1  8902  lble  9126  zaddcllemneg  9517  fnn0ind  9595  xrltso  10030  iccgelb  10166  elicc4  10174  elfz  10248  fzrevral  10339  expnegap0  10808  expgt0  10833  expge0  10836  expge1  10837  mulexpzap  10840  expp1zap  10849  expm1ap  10850  apexp1  10979  ccatsymb  11178  abssubap0  11650  binom  12044  dvds0lem  12361  dvdsnegb  12368  muldvds1  12376  muldvds2  12377  divalgmodcl  12488  gcd2n0cl  12539  lcmdvds  12650  prmdvdsexp  12719  rpexp1i  12725  eqglact  13811  lss0cl  14382  cnpval  14921  cnf2  14928  cnnei  14955  blssec  15161  blpnfctr  15162  mopni2  15206  mopni3  15207  dvply1  15488  uhgrm  15928  upgrm  15950  upgr1or2  15951