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  2623  rspc3v  2927  raltpg  3726  rextpg  3727  disjiun  4088  otexg  4328  opelopabt  4362  tpexg  4547  3optocl  4810  fun2ssres  5377  funssfv  5674  fvun1  5721  foco2  5904  f1elima  5924  eloprabga  6118  caovimo  6226  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  brtposg  6463  rdgexggg  6586  rdgivallem  6590  nnmass  6698  nndir  6701  nnaword  6722  th3q  6852  ecovass  6856  ecoviass  6857  fpmg  6886  findcard  7120  unfiin  7161  pr1or2  7442  addasspig  7593  mulasspig  7595  mulcanpig  7598  ltapig  7601  ltmpig  7602  addassnqg  7645  ltbtwnnqq  7678  mulnnnq0  7713  addassnq0  7725  genpassl  7787  genpassu  7788  genpassg  7789  aptiprleml  7902  adddir  8213  le2tri3i  8330  addsub12  8434  subdir  8607  reapmul1  8817  recexaplem2  8874  div12ap  8916  divdiv32ap  8942  divdivap1  8945  lble  9169  zaddcllemneg  9562  fnn0ind  9640  xrltso  10075  iccgelb  10211  elicc4  10219  elfz  10294  fzrevral  10385  expnegap0  10855  expgt0  10880  expge0  10883  expge1  10884  mulexpzap  10887  expp1zap  10896  expm1ap  10897  apexp1  11026  ccatsymb  11228  abssubap0  11713  binom  12108  dvds0lem  12425  dvdsnegb  12432  muldvds1  12440  muldvds2  12441  divalgmodcl  12552  gcd2n0cl  12603  lcmdvds  12714  prmdvdsexp  12783  rpexp1i  12789  eqglact  13875  lss0cl  14448  cnpval  14992  cnf2  14999  cnnei  15026  blssec  15232  blpnfctr  15233  mopni2  15277  mopni3  15278  dvply1  15559  uhgrm  16002  upgrm  16024  upgr1or2  16025