Theorem imp32 418

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imp42  426  impr  454  anasss  466  an13s  652  3expb  1121  reuss2  4266  reupick  4269  po2nr  5553  tz7.7  6349  ordtr2  6368  fvmptt  6968  fliftfund  7268  isomin  7292  f1ocnv2d  7620  onint  7744  resf1extb  7885  soseq  8109  tz7.48lem  8380  oalimcl  8495  oaass  8496  omass  8515  omabs  8587  finsschain  9269  frmin  9673  infxpenlem  9935  axcc3  10360  zorn2lem7  10424  addclpi  10815  addnidpi  10824  genpnnp  10928  genpnmax  10930  mulclprlem  10942  dedekindle  11310  prodgt0  12002  ltsubrp  12980  ltaddrp  12981  pfxccat3  14696  sumeven  16356  sumodd  16357  lcmfunsnlem2lem1  16607  divgcdcoprm0  16634  infpnlem1  16881  prmgaplem4  17025  iscatd  17639  imasmnd2  18742  imasgrp2  19031  cyccom  19178  imasrng  20158  imasring  20310  funcrngcsetcALT  20618  mplcoe5lem  22017  dmatmul  22462  scmatmulcl  22483  scmatsgrp1  22487  smatvscl  22489  cpmatacl  22681  cpmatmcllem  22683  0ntr  23036  clsndisj  23040  innei  23090  islpi  23114  tgcnp  23218  haust1  23317  alexsublem  24009  alexsubb  24011  isxmetd  24291  bddiblnc  25809  2lgslem1a1  27352  nodense  27656  precsexlem11  28209  bdaypw2n0bndlem  28455  axcontlem4  29036  ewlkle  29674  clwwlkf  30117  clwwlknonwwlknonb  30176  uhgr3cyclexlem  30251  numclwwlk1lem2foa  30424  grpoidinvlem3  30577  elspansn5  31645  5oalem6  31730  mdi  32366  dmdi  32373  dmdsl3  32386  atom1d  32424  cvexchlem  32439  atcvatlem  32456  chirredlem3  32463  mdsymlem5  32478  f1o3d  32699  bnj570  35047  dfon2lem6  35968  broutsideof2  36304  outsideoftr  36311  outsideofeq  36312  elicc3  36499  nn0prpwlem  36504  nndivsub  36639  fvineqsneu  37727  fvineqsneq  37728  ftc1anc  38022  cntotbnd  38117  heiborlem6  38137  pridlc3  38394  erimeq2  39084  leat2  39740  cvrexchlem  39865  cvratlem  39867  3dim2  39914  ps-2  39924  lncvrelatN  40227  osumcllem11N  40412  relpmin  45379  2reuimp0  47562  iccpartgt  47887  odz2prm2pw  48026  bgoldbachlt  48289  tgblthelfgott  48291  tgoldbach  48293  grimco  48365  isubgr3stgrlem6  48447  isubgr3stgrlem8  48449  uspgrlimlem2  48465  clnbgr3stgrgrlic  48496  gpgedgvtx0  48537  gpgedgvtx1  48538