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  4316  reupick  4319  po2nr  5603  tz7.7  6391  ordtr2  6409  fvmptt  7019  fliftfund  7310  isomin  7334  f1ocnv2d  7659  onint  7778  soseq  8145  tz7.48lem  8441  oalimcl  8560  oaass  8561  omass  8580  omabs  8650  finsschain  9359  frmin  9744  infxpenlem  10008  axcc3  10433  zorn2lem7  10497  addclpi  10887  addnidpi  10896  genpnnp  11000  genpnmax  11002  mulclprlem  11014  dedekindle  11378  prodgt0  12061  ltsubrp  13010  ltaddrp  13011  pfxccat3  14684  sumeven  16330  sumodd  16331  lcmfunsnlem2lem1  16575  divgcdcoprm0  16602  infpnlem1  16843  prmgaplem4  16987  iscatd  17617  imasmnd2  18662  imasgrp2  18938  cyccom  19080  imasring  20143  mplcoe5lem  21594  dmatmul  21999  scmatmulcl  22020  scmatsgrp1  22024  smatvscl  22026  cpmatacl  22218  cpmatmcllem  22220  0ntr  22575  clsndisj  22579  innei  22629  islpi  22653  tgcnp  22757  haust1  22856  alexsublem  23548  alexsubb  23550  isxmetd  23832  bddiblnc  25359  2lgslem1a1  26892  nodense  27195  precsexlem11  27663  axcontlem4  28225  ewlkle  28862  clwwlkf  29300  clwwlknonwwlknonb  29359  uhgr3cyclexlem  29434  numclwwlk1lem2foa  29607  grpoidinvlem3  29759  elspansn5  30827  5oalem6  30912  mdi  31548  dmdi  31555  dmdsl3  31568  atom1d  31606  cvexchlem  31621  atcvatlem  31638  chirredlem3  31645  mdsymlem5  31660  f1o3d  31851  bnj570  33916  dfon2lem6  34760  broutsideof2  35094  outsideoftr  35101  outsideofeq  35102  elicc3  35202  nn0prpwlem  35207  nndivsub  35342  fvineqsneu  36292  fvineqsneq  36293  ftc1anc  36569  cntotbnd  36664  heiborlem6  36684  pridlc3  36941  erimeq2  37548  leat2  38164  cvrexchlem  38290  cvratlem  38292  3dim2  38339  ps-2  38349  lncvrelatN  38652  osumcllem11N  38837  2reuimp0  45822  iccpartgt  46095  odz2prm2pw  46231  bgoldbachlt  46481  tgblthelfgott  46483  tgoldbach  46485  isomgrsym  46504  isomgrtr  46507  imasrng  46678  funcrngcsetcALT  46897