Theorem imp32 420

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 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 408	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imp42  428  impr  456  anasss  468  an13s  650  3expb  1121  reuss2  4315  reupick  4318  po2nr  5602  tz7.7  6388  ordtr2  6406  fvmptt  7016  fliftfund  7307  isomin  7331  f1ocnv2d  7656  onint  7775  soseq  8142  tz7.48lem  8438  oalimcl  8557  oaass  8558  omass  8577  omabs  8647  finsschain  9356  frmin  9741  infxpenlem  10005  axcc3  10430  zorn2lem7  10494  addclpi  10884  addnidpi  10893  genpnnp  10997  genpnmax  10999  mulclprlem  11011  dedekindle  11375  prodgt0  12058  ltsubrp  13007  ltaddrp  13008  pfxccat3  14681  sumeven  16327  sumodd  16328  lcmfunsnlem2lem1  16572  divgcdcoprm0  16599  infpnlem1  16840  prmgaplem4  16984  iscatd  17614  imasmnd2  18659  imasgrp2  18935  cyccom  19075  imasring  20137  mplcoe5lem  21586  dmatmul  21991  scmatmulcl  22012  scmatsgrp1  22016  smatvscl  22018  cpmatacl  22210  cpmatmcllem  22212  0ntr  22567  clsndisj  22571  innei  22621  islpi  22645  tgcnp  22749  haust1  22848  alexsublem  23540  alexsubb  23542  isxmetd  23824  bddiblnc  25351  2lgslem1a1  26882  nodense  27185  precsexlem11  27653  axcontlem4  28215  ewlkle  28852  clwwlkf  29290  clwwlknonwwlknonb  29349  uhgr3cyclexlem  29424  numclwwlk1lem2foa  29597  grpoidinvlem3  29747  elspansn5  30815  5oalem6  30900  mdi  31536  dmdi  31543  dmdsl3  31556  atom1d  31594  cvexchlem  31609  atcvatlem  31626  chirredlem3  31633  mdsymlem5  31648  f1o3d  31839  bnj570  33905  dfon2lem6  34749  broutsideof2  35083  outsideoftr  35090  outsideofeq  35091  elicc3  35191  nn0prpwlem  35196  nndivsub  35331  fvineqsneu  36281  fvineqsneq  36282  ftc1anc  36558  cntotbnd  36653  heiborlem6  36673  pridlc3  36930  erimeq2  37537  leat2  38153  cvrexchlem  38279  cvratlem  38281  3dim2  38328  ps-2  38338  lncvrelatN  38641  osumcllem11N  38826  2reuimp0  45809  iccpartgt  46082  odz2prm2pw  46218  bgoldbachlt  46468  tgblthelfgott  46470  tgoldbach  46472  isomgrsym  46491  isomgrtr  46494  imasrng  46665  funcrngcsetcALT  46851