Theorem 3impa 1218

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

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

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 1004

This theorem is referenced by:  ex3  1219  3impdir  1328  syl3an9b  1344  biimp3a  1379  stoic3  1473  rspec3  2620  rspc3v  2924  raltpg  3720  rextpg  3721  disjiun  4081  otexg  4320  opelopabt  4354  tpexg  4539  3optocl  4802  fun2ssres  5367  funssfv  5661  fvun1  5708  foco2  5889  f1elima  5909  eloprabga  6103  caovimo  6211  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  brtposg  6415  rdgexggg  6538  rdgivallem  6542  nnmass  6650  nndir  6653  nnaword  6674  th3q  6804  ecovass  6808  ecoviass  6809  fpmg  6838  findcard  7070  unfiin  7111  pr1or2  7390  addasspig  7540  mulasspig  7542  mulcanpig  7545  ltapig  7548  ltmpig  7549  addassnqg  7592  ltbtwnnqq  7625  mulnnnq0  7660  addassnq0  7672  genpassl  7734  genpassu  7735  genpassg  7736  aptiprleml  7849  adddir  8160  le2tri3i  8278  addsub12  8382  subdir  8555  reapmul1  8765  recexaplem2  8822  div12ap  8864  divdiv32ap  8890  divdivap1  8893  lble  9117  zaddcllemneg  9508  fnn0ind  9586  xrltso  10021  iccgelb  10157  elicc4  10165  elfz  10239  fzrevral  10330  expnegap0  10799  expgt0  10824  expge0  10827  expge1  10828  mulexpzap  10831  expp1zap  10840  expm1ap  10841  apexp1  10970  ccatsymb  11169  abssubap0  11641  binom  12035  dvds0lem  12352  dvdsnegb  12359  muldvds1  12367  muldvds2  12368  divalgmodcl  12479  gcd2n0cl  12530  lcmdvds  12641  prmdvdsexp  12710  rpexp1i  12716  eqglact  13802  lss0cl  14373  cnpval  14912  cnf2  14919  cnnei  14946  blssec  15152  blpnfctr  15153  mopni2  15197  mopni3  15198  dvply1  15479  uhgrm  15919  upgrm  15941  upgr1or2  15942