Theorem imp32 424

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp42  432  impr  460  anasss  472  an13s  664  3expb  1138  reuss2  4270  reupick  4273  po2nr  5573  tz7.7  6391  ordtr2  6411  fvmptt  7019  fliftfund  7325  isomin  7349  f1ocnv2d  7678  onint  7808  resf1extb  7950  soseq  8182  tz7.48lemOLD  8458  oalimcl  8575  oaass  8576  omass  8595  omabs  8667  finsschain  9355  frmin  9760  infxpenlem  10099  axcc3  10523  zorn2lem7  10587  addclpi  10984  addnidpi  10993  genpnnp  11097  genpnmax  11099  mulclprlem  11111  dedekindle  11481  prodgt0  12171  ltsubrp  13165  ltaddrp  13166  pfxccat3  14891  sumeven  16566  sumodd  16567  lcmfunsnlem2lem1  16822  divgcdcoprm0  16849  infpnlem1  17097  prmgaplem4  17241  iscatd  17856  mgmn0plusgf  18836  imasmnd2  18977  imasgrp2  19274  cyccom  19427  imasrng  20408  imasring  20569  funcrngcsetcALT  20902  cmprmidlmcl  21640  mplcoe5lem  22357  dmatmul  22821  scmatmulcl  22842  scmatsgrp1  22846  smatvscl  22848  cpmatacl  23043  cpmatmcllem  23045  0ntr  23398  clsndisj  23402  innei  23452  islpi  23476  tgcnp  23580  haust1  23679  alexsublem  24372  alexsubb  24374  isxmetd  24654  bddiblnc  26171  2lgslem1a1  27725  nodense  28058  precsexlem11  28612  bdaypw2n0bndlem  28858  axcontlem4  29554  ewlkle  30195  clwwlkf  30647  clwwlknonwwlknonb  30706  uhgr3cyclexlem  30791  numclwwlk1lem2foa  30964  grpoidinvlem3  31117  elspansn5  32185  5oalem6  32270  mdi  32906  dmdi  32913  dmdsl3  32926  atom1d  32964  cvexchlem  32979  atcvatlem  32996  chirredlem3  33003  mdsymlem5  33018  f1o3d  33271  bnj570  35585  dfon2lem6  36646  broutsideof2  36983  outsideoftr  36990  outsideofeq  36991  elicc3  37201  nn0prpwlem  37206  nndivsub  37341  fvineqsneu  38443  fvineqsneq  38444  ftc1anc  38728  cntotbnd  38839  heiborlem6  38859  pridlc3  39116  erimeq2  39804  leat2  40460  cvrexchlem  40585  cvratlem  40587  3dim2  40634  ps-2  40644  lncvrelatN  40947  osumcllem11N  41132  relpmin  46050  2reuimp0  48293  iccpartgt  48617  odz2prm2pw  48756  bgoldbachlt  49019  tgblthelfgott  49021  tgoldbach  49023  grimco  49095  isubgr3stgrlem6  49177  isubgr3stgrlem8  49179  uspgrlimlem2  49195  clnbgr3stgrgrlic  49226  gpgedgvtx0  49267  gpgedgvtx1  49268