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  4274  reupick  4277  po2nr  5580  tz7.7  6414  ordtr2  6434  fvmptt  7045  fliftfund  7352  isomin  7376  f1ocnv2d  7706  onint  7838  resf1extb  7980  soseq  8213  tz7.48lemOLD  8489  oalimcl  8606  oaass  8607  omass  8626  omabs  8698  finsschain  9386  frmin  9790  infxpenlem  10131  axcc3  10555  zorn2lem7  10619  addclpi  11016  addnidpi  11025  genpnnp  11129  genpnmax  11131  mulclprlem  11143  dedekindle  11513  prodgt0  12204  ltsubrp  13198  ltaddrp  13199  pfxccat3  14925  sumeven  16601  sumodd  16602  lcmfunsnlem2lem1  16857  divgcdcoprm0  16884  infpnlem1  17132  prmgaplem4  17276  iscatd  17897  mgmn0plusgf  18877  imasmnd2  19018  imasgrp2  19315  cyccom  19468  imasrng  20450  imasring  20611  funcrngcsetcALT  20944  cmprmidlmcl  21682  mplcoe5lem  22403  dmatmul  22867  scmatmulcl  22888  scmatsgrp1  22892  smatvscl  22894  cpmatacl  23089  cpmatmcllem  23091  0ntr  23444  clsndisj  23448  innei  23498  islpi  23522  tgcnp  23626  haust1  23725  alexsublem  24418  alexsubb  24420  isxmetd  24700  bddiblnc  26217  2lgslem1a1  27773  nodense  28106  precsexlem11  28660  bdaypw2n0bndlem  28906  axcontlem4  29602  ewlkle  30243  clwwlkf  30695  clwwlknonwwlknonb  30754  uhgr3cyclexlem  30839  numclwwlk1lem2foa  31012  grpoidinvlem3  31165  elspansn5  32233  5oalem6  32318  mdi  32954  dmdi  32961  dmdsl3  32974  atom1d  33012  cvexchlem  33027  atcvatlem  33044  chirredlem3  33051  mdsymlem5  33066  f1o3d  33318  bnj570  35646  dfon2lem6  36765  broutsideof2  37102  outsideoftr  37109  outsideofeq  37110  elicc3  37320  nn0prpwlem  37325  nndivsub  37460  fvineqsneu  38602  fvineqsneq  38603  ftc1anc  38887  cntotbnd  38996  heiborlem6  39016  pridlc3  39273  erimeq2  39961  leat2  40617  cvrexchlem  40742  cvratlem  40744  3dim2  40791  ps-2  40801  lncvrelatN  41104  osumcllem11N  41289  relpmin  46206  2reuimp0  48458  iccpartgt  48782  odz2prm2pw  48921  bgoldbachlt  49184  tgblthelfgott  49186  tgoldbach  49188  grimco  49260  isubgr3stgrlem6  49342  isubgr3stgrlem8  49344  uspgrlimlem2  49360  clnbgr3stgrgrlic  49391  gpgedgvtx0  49432  gpgedgvtx1  49433  lazsubcl  49739