Theorem imp32 409

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp31.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp32	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp31.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 398	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 395	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 198  df-an 385

This theorem is referenced by:  imp42  417  impr  446  anasss  458  an13s  641  3expb  1149  reuss2  4073  reupick  4077  po2nr  5213  tz7.7  5936  ordtr2  5954  fvmptt  6493  fliftfund  6759  isomin  6783  f1ocnv2d  7088  onint  7197  tz7.48lem  7744  oalimcl  7849  oaass  7850  omass  7869  omabs  7936  finsschain  8484  infxpenlem  9091  axcc3  9517  zorn2lem7  9581  addclpi  9971  addnidpi  9980  genpnnp  10084  genpnmax  10086  mulclprlem  10098  dedekindle  10459  prodgt0  11126  ltsubrp  12069  ltaddrp  12070  swrdccatin1  13743  pfxccat3  13755  swrdccat3OLD  13756  sumeven  15406  sumodd  15407  lcmfunsnlem2lem1  15646  divgcdcoprm0  15673  infpnlem1  15907  prmgaplem4  16051  iscatd  16613  imasmnd2  17607  imasgrp2  17811  imasring  18900  mplcoe5lem  19755  dmatmul  20594  scmatmulcl  20615  scmatsgrp1  20619  smatvscl  20621  cpmatacl  20814  cpmatmcllem  20816  0ntr  21169  clsndisj  21173  innei  21223  islpi  21247  tgcnp  21351  haust1  21450  alexsublem  22141  alexsubb  22143  isxmetd  22424  2lgslem1a1  25419  axcontlem4  26152  ewlkle  26806  wlkwwlksurOLD  27108  clwwlkfOLD  27308  clwwlkf  27313  clwwlknonwwlknonb  27397  clwwlknonwwlknonbOLD  27398  uhgr3cyclexlem  27477  numclwwlk2lem1lemOLD  27645  numclwwlk1lem2foa  27666  numclwwlk1lem2foaOLD  27667  grpoidinvlem3  27838  elspansn5  28910  5oalem6  28995  mdi  29631  dmdi  29638  dmdsl3  29651  atom1d  29689  cvexchlem  29704  atcvatlem  29721  chirredlem3  29728  mdsymlem5  29743  f1o3d  29902  bnj570  31444  dfon2lem6  32157  frmin  32207  soseq  32219  nodense  32307  broutsideof2  32694  outsideoftr  32701  outsideofeq  32702  elicc3  32776  nn0prpwlem  32781  nndivsub  32916  bddiblnc  33924  ftc1anc  33937  cntotbnd  34038  heiborlem6  34058  pridlc3  34315  leat2  35271  cvrexchlem  35396  cvratlem  35398  3dim2  35445  ps-2  35455  lncvrelatN  35758  osumcllem11N  35943  iccpartgt  42121  odz2prm2pw  42175  bgoldbachlt  42401  tgblthelfgott  42403  tgoldbach  42405  funcrngcsetcALT  42692