Theorem imp32 422

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  imp42  430  impr  458  anasss  470  an13s  651  3expb  1122  reuss2  4216  reupick  4219  po2nr  5467  tz7.7  6217  ordtr2  6235  fvmptt  6816  fliftfund  7100  isomin  7124  f1ocnv2d  7436  onint  7552  tz7.48lem  8155  oalimcl  8266  oaass  8267  omass  8286  omabs  8354  finsschain  8961  infxpenlem  9592  axcc3  10017  zorn2lem7  10081  addclpi  10471  addnidpi  10480  genpnnp  10584  genpnmax  10586  mulclprlem  10598  dedekindle  10961  prodgt0  11644  ltsubrp  12587  ltaddrp  12588  pfxccat3  14264  sumeven  15911  sumodd  15912  lcmfunsnlem2lem1  16158  divgcdcoprm0  16185  infpnlem1  16426  prmgaplem4  16570  iscatd  17130  imasmnd2  18164  imasgrp2  18432  cyccom  18564  imasring  19591  mplcoe5lem  20950  dmatmul  21348  scmatmulcl  21369  scmatsgrp1  21373  smatvscl  21375  cpmatacl  21567  cpmatmcllem  21569  0ntr  21922  clsndisj  21926  innei  21976  islpi  22000  tgcnp  22104  haust1  22203  alexsublem  22895  alexsubb  22897  isxmetd  23178  bddiblnc  24693  2lgslem1a1  26224  axcontlem4  27012  ewlkle  27647  clwwlkf  28084  clwwlknonwwlknonb  28143  uhgr3cyclexlem  28218  numclwwlk1lem2foa  28391  grpoidinvlem3  28541  elspansn5  29609  5oalem6  29694  mdi  30330  dmdi  30337  dmdsl3  30350  atom1d  30388  cvexchlem  30403  atcvatlem  30420  chirredlem3  30427  mdsymlem5  30442  f1o3d  30635  bnj570  32552  dfon2lem6  33434  frmin  33459  soseq  33483  nodense  33581  broutsideof2  34110  outsideoftr  34117  outsideofeq  34118  elicc3  34192  nn0prpwlem  34197  nndivsub  34332  fvineqsneu  35268  fvineqsneq  35269  ftc1anc  35544  cntotbnd  35640  heiborlem6  35660  pridlc3  35917  erim2  36475  leat2  36994  cvrexchlem  37119  cvratlem  37121  3dim2  37168  ps-2  37178  lncvrelatN  37481  osumcllem11N  37666  2reuimp0  44221  iccpartgt  44495  odz2prm2pw  44631  bgoldbachlt  44881  tgblthelfgott  44883  tgoldbach  44885  isomgrsym  44904  isomgrtr  44907  funcrngcsetcALT  45173