Theorem 3impa 1196

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

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

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 982

This theorem is referenced by:  ex3  1197  3impdir  1305  syl3an9b  1321  biimp3a  1356  stoic3  1442  rspec3  2587  rspc3v  2884  raltpg  3676  rextpg  3677  disjiun  4029  otexg  4264  opelopabt  4297  tpexg  4480  3optocl  4742  fun2ssres  5302  funssfv  5587  fvun1  5630  foco2  5803  f1elima  5823  eloprabga  6013  caovimo  6121  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  brtposg  6321  rdgexggg  6444  rdgivallem  6448  nnmass  6554  nndir  6557  nnaword  6578  th3q  6708  ecovass  6712  ecoviass  6713  fpmg  6742  findcard  6958  unfiin  6996  addasspig  7416  mulasspig  7418  mulcanpig  7421  ltapig  7424  ltmpig  7425  addassnqg  7468  ltbtwnnqq  7501  mulnnnq0  7536  addassnq0  7548  genpassl  7610  genpassu  7611  genpassg  7612  aptiprleml  7725  adddir  8036  le2tri3i  8154  addsub12  8258  subdir  8431  reapmul1  8641  recexaplem2  8698  div12ap  8740  divdiv32ap  8766  divdivap1  8769  lble  8993  zaddcllemneg  9384  fnn0ind  9461  xrltso  9890  iccgelb  10026  elicc4  10034  elfz  10108  fzrevral  10199  expnegap0  10658  expgt0  10683  expge0  10686  expge1  10687  mulexpzap  10690  expp1zap  10699  expm1ap  10700  apexp1  10829  abssubap0  11274  binom  11668  dvds0lem  11985  dvdsnegb  11992  muldvds1  12000  muldvds2  12001  divalgmodcl  12112  gcd2n0cl  12163  lcmdvds  12274  prmdvdsexp  12343  rpexp1i  12349  eqglact  13433  lss0cl  14003  cnpval  14542  cnf2  14549  cnnei  14576  blssec  14782  blpnfctr  14783  mopni2  14827  mopni3  14828  dvply1  15109