Theorem imp31 422

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp31.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp31	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp31.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	imp 411	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 411	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  imp41  430  imp5d  444  impl  460  anassrs  472  an31s  666  3imp  1126  reusv3  5377  otiunsndisj  5504  pwssun  5554  ordelord  6383  tz7.7  6387  dfimafn  6944  funimass4  6946  funimass3  7050  isomin  7336  isopolem  7344  onint  7789  limsssuc  7846  tfindsg  7857  findsg  7894  suppfnss  8185  smores2  8341  tfrlem9  8372  tz7.49  8432  oecl  8522  oaordi  8531  oaass  8546  omordi  8551  odi  8564  oen0  8572  nnaordi  8604  nnmordi  8617  domunfican  9281  dfac5  10112  cofsmo  10253  cfcoflem  10256  zorn2lem7  10486  tskwun  10769  mulcanpi  10885  ltexprlem7  11027  sup3  12172  elnnz  12601  nzadd  12642  irradd  12997  irrmul  12998  uzsubsubfz  13574  fzo1fzo0n0  13744  elincfzoext  13752  elfzonelfzo  13798  uzindi  14018  ssnn0fi  14021  sqlecan  14245  swrdnd2  14693  swrdwrdsymb  14700  wrd2ind  14760  repswccat  14823  cshwlen  14836  cshwidxmod  14840  2cshwcshw  14862  wrdl3s3  14999  lcmfunsnlem1  16695  coprmprod  16719  unbenlem  16968  infpnlem1  16970  prmgaplem7  17117  iscatd  17729  dirtr  18658  telgsums  20063  zrtermorngc  20728  zrtermoringc  20760  prmidlc  21444  psgndiflemA  21720  isphld  21773  gsummoncoe1  22437  gsummatr01lem3  22783  cpmatmcllem  22844  mp2pm2mplem4  22935  chfacfisf  22980  chfacfisfcpmat  22981  cayleyhamilton1  23018  tgcl  23095  neindisj2  23249  2ndcdisj  23582  fgcl  24004  rnelfm  24079  alexsubALTlem3  24175  2sqreultlem  27577  2sqreunnltlem  27580  elnnzs  28560  usgrexmpledg  29553  cusgrsize  29745  uspgr2wlkeqi  29938  usgr2wlkneq  30046  usgr2pthlem  30053  crctcshwlkn0  30111  wwlksnextinj  30189  wwlksnextproplem2  30200  wwlksnextproplem3  30201  clwlkclwwlklem2a  30290  clwlkclwwlklem2  30292  clwwlkf1  30341  clwwlknwwlksnb  30347  clwwlkext2edg  30348  clwwlknonex2lem2  30400  frgr3vlem1  30565  3vfriswmgrlem  30569  vdgn1frgrv2  30588  frgrwopreglem5  30613  frgrwopreglem5ALT  30614  mdexchi  32628  atomli  32675  mdsymlem5  32700  sumdmdlem  32711  dfimafnf  32922  bnj517  35218  bnj1118  35317  mclsind  35961  dfon2lem6  36177  btwnconn1lem11  36488  finminlem  36718  isbasisrelowllem1  37889  isbasisrelowllem2  37890  poimirlem27  38186  itg2addnc  38213  rngoueqz  38479  dmncan1  38615  disjlem19  39443  lshpdisj  39651  2at0mat0  40189  llncvrlpln2  40221  lplncvrlvol2  40279  pmaple  40425  lhpexle2lem  40673  cdlemk33N  41573  cdlemk34  41574  sn-sup3d  43156  eldioph2  43385  cantnfresb  43943  gneispacess2  44764  sge0iunmpt  47024  funressnfv  47669  dfaimafn  47791  otiunsndisjX  47905  elfz2z  47941  iccelpart  48071  icceuelpart  48074  fargshiftfva  48081  sprsymrelfo  48135  sbcpr  48159  bgoldbtbndlem4  48462  grimcnv  48542  grimco  48543  clnbgrgrim  48588  uspgrlimlem4  48645  grlicsym  48667  grlictr  48669  pgnbgreunbgrlem3  48772  pgnbgreunbgrlem6  48778  snlindsntor  49136  ldepspr  49138  nn0sumshdiglemB  49285