Theorem 3impa 1197

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

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

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 983

This theorem is referenced by:  ex3  1198  3impdir  1307  syl3an9b  1323  biimp3a  1358  stoic3  1451  rspec3  2598  rspc3v  2900  raltpg  3696  rextpg  3697  disjiun  4054  otexg  4292  opelopabt  4326  tpexg  4509  3optocl  4771  fun2ssres  5333  funssfv  5625  fvun1  5668  foco2  5845  f1elima  5865  eloprabga  6055  caovimo  6163  ot1stg  6261  ot2ndg  6262  ot3rdgg  6263  brtposg  6363  rdgexggg  6486  rdgivallem  6490  nnmass  6596  nndir  6599  nnaword  6620  th3q  6750  ecovass  6754  ecoviass  6755  fpmg  6784  findcard  7011  unfiin  7049  pr1or2  7328  addasspig  7478  mulasspig  7480  mulcanpig  7483  ltapig  7486  ltmpig  7487  addassnqg  7530  ltbtwnnqq  7563  mulnnnq0  7598  addassnq0  7610  genpassl  7672  genpassu  7673  genpassg  7674  aptiprleml  7787  adddir  8098  le2tri3i  8216  addsub12  8320  subdir  8493  reapmul1  8703  recexaplem2  8760  div12ap  8802  divdiv32ap  8828  divdivap1  8831  lble  9055  zaddcllemneg  9446  fnn0ind  9524  xrltso  9953  iccgelb  10089  elicc4  10097  elfz  10171  fzrevral  10262  expnegap0  10729  expgt0  10754  expge0  10757  expge1  10758  mulexpzap  10761  expp1zap  10770  expm1ap  10771  apexp1  10900  ccatsymb  11096  abssubap0  11516  binom  11910  dvds0lem  12227  dvdsnegb  12234  muldvds1  12242  muldvds2  12243  divalgmodcl  12354  gcd2n0cl  12405  lcmdvds  12516  prmdvdsexp  12585  rpexp1i  12591  eqglact  13676  lss0cl  14246  cnpval  14785  cnf2  14792  cnnei  14819  blssec  15025  blpnfctr  15026  mopni2  15070  mopni3  15071  dvply1  15352  uhgrm  15789  upgrm  15811  upgr1or2  15812