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  2923  raltpg  3719  rextpg  3720  disjiun  4078  otexg  4316  opelopabt  4350  tpexg  4535  3optocl  4797  fun2ssres  5361  funssfv  5655  fvun1  5702  foco2  5883  f1elima  5903  eloprabga  6097  caovimo  6205  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  brtposg  6406  rdgexggg  6529  rdgivallem  6533  nnmass  6641  nndir  6644  nnaword  6665  th3q  6795  ecovass  6799  ecoviass  6800  fpmg  6829  findcard  7058  unfiin  7099  pr1or2  7378  addasspig  7528  mulasspig  7530  mulcanpig  7533  ltapig  7536  ltmpig  7537  addassnqg  7580  ltbtwnnqq  7613  mulnnnq0  7648  addassnq0  7660  genpassl  7722  genpassu  7723  genpassg  7724  aptiprleml  7837  adddir  8148  le2tri3i  8266  addsub12  8370  subdir  8543  reapmul1  8753  recexaplem2  8810  div12ap  8852  divdiv32ap  8878  divdivap1  8881  lble  9105  zaddcllemneg  9496  fnn0ind  9574  xrltso  10004  iccgelb  10140  elicc4  10148  elfz  10222  fzrevral  10313  expnegap0  10781  expgt0  10806  expge0  10809  expge1  10810  mulexpzap  10813  expp1zap  10822  expm1ap  10823  apexp1  10952  ccatsymb  11150  abssubap0  11616  binom  12010  dvds0lem  12327  dvdsnegb  12334  muldvds1  12342  muldvds2  12343  divalgmodcl  12454  gcd2n0cl  12505  lcmdvds  12616  prmdvdsexp  12685  rpexp1i  12691  eqglact  13777  lss0cl  14348  cnpval  14887  cnf2  14894  cnnei  14921  blssec  15127  blpnfctr  15128  mopni2  15172  mopni3  15173  dvply1  15454  uhgrm  15893  upgrm  15915  upgr1or2  15916