Theorem imp32 417

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  imp42  425  impr  453  anasss  465  an13s  649  3expb  1117  reuss2  4315  reupick  4318  po2nr  5604  tz7.7  6397  ordtr2  6415  fvmptt  7024  fliftfund  7320  isomin  7344  f1ocnv2d  7674  onint  7794  soseq  8164  tz7.48lem  8462  oalimcl  8581  oaass  8582  omass  8601  omabs  8672  finsschain  9385  frmin  9774  infxpenlem  10038  axcc3  10463  zorn2lem7  10527  addclpi  10917  addnidpi  10926  genpnnp  11030  genpnmax  11032  mulclprlem  11044  dedekindle  11410  prodgt0  12094  ltsubrp  13045  ltaddrp  13046  pfxccat3  14720  sumeven  16367  sumodd  16368  lcmfunsnlem2lem1  16612  divgcdcoprm0  16639  infpnlem1  16882  prmgaplem4  17026  iscatd  17656  imasmnd2  18734  imasgrp2  19019  cyccom  19166  imasrng  20129  imasring  20278  funcrngcsetcALT  20586  mplcoe5lem  21999  dmatmul  22443  scmatmulcl  22464  scmatsgrp1  22468  smatvscl  22470  cpmatacl  22662  cpmatmcllem  22664  0ntr  23019  clsndisj  23023  innei  23073  islpi  23097  tgcnp  23201  haust1  23300  alexsublem  23992  alexsubb  23994  isxmetd  24276  bddiblnc  25815  2lgslem1a1  27367  nodense  27671  precsexlem11  28165  axcontlem4  28850  ewlkle  29491  clwwlkf  29929  clwwlknonwwlknonb  29988  uhgr3cyclexlem  30063  numclwwlk1lem2foa  30236  grpoidinvlem3  30388  elspansn5  31456  5oalem6  31541  mdi  32177  dmdi  32184  dmdsl3  32197  atom1d  32235  cvexchlem  32250  atcvatlem  32267  chirredlem3  32274  mdsymlem5  32289  f1o3d  32493  bnj570  34667  dfon2lem6  35515  broutsideof2  35849  outsideoftr  35856  outsideofeq  35857  elicc3  35932  nn0prpwlem  35937  nndivsub  36072  fvineqsneu  37021  fvineqsneq  37022  ftc1anc  37305  cntotbnd  37400  heiborlem6  37420  pridlc3  37677  erimeq2  38280  leat2  38896  cvrexchlem  39022  cvratlem  39024  3dim2  39071  ps-2  39081  lncvrelatN  39384  osumcllem11N  39569  2reuimp0  46632  iccpartgt  46904  odz2prm2pw  47040  bgoldbachlt  47290  tgblthelfgott  47292  tgoldbach  47294  grimco  47364