Theorem imp31 417

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imp41  425  imp5d  439  impl  455  anassrs  467  an31s  654  3imp  1110  reusv3  5341  otiunsndisj  5458  pwssun  5506  ordelord  6328  tz7.7  6332  dfimafn  6884  funimass4  6886  funimass3  6987  isomin  7271  isopolem  7279  onint  7723  limsssuc  7780  tfindsg  7791  findsg  7827  suppfnss  8119  smores2  8274  tfrlem9  8304  tz7.49  8364  oecl  8452  oaordi  8461  oaass  8476  omordi  8481  odi  8494  oen0  8501  nnaordi  8533  nnmordi  8546  domunfican  9206  dfac5  10020  cofsmo  10160  cfcoflem  10163  zorn2lem7  10393  tskwun  10675  mulcanpi  10791  ltexprlem7  10933  sup3  12079  elnnz  12478  nzadd  12520  irradd  12871  irrmul  12872  uzsubsubfz  13446  fzo1fzo0n0  13615  elincfzoext  13623  elfzonelfzo  13669  uzindi  13889  ssnn0fi  13892  sqlecan  14116  swrdnd2  14563  swrdwrdsymb  14570  wrd2ind  14630  repswccat  14693  cshwlen  14706  cshwidxmod  14710  2cshwcshw  14732  wrdl3s3  14869  lcmfunsnlem1  16548  coprmprod  16572  unbenlem  16820  infpnlem1  16822  prmgaplem7  16969  iscatd  17579  dirtr  18508  telgsums  19905  zrtermorngc  20558  zrtermoringc  20590  psgndiflemA  21538  isphld  21591  gsummoncoe1  22223  gsummatr01lem3  22572  cpmatmcllem  22633  mp2pm2mplem4  22724  chfacfisf  22769  chfacfisfcpmat  22770  cayleyhamilton1  22807  tgcl  22884  neindisj2  23038  2ndcdisj  23371  fgcl  23793  rnelfm  23868  alexsubALTlem3  23964  2sqreultlem  27385  2sqreunnltlem  27388  elnnzs  28325  usgrexmpledg  29240  cusgrsize  29433  uspgr2wlkeqi  29626  usgr2wlkneq  29734  usgr2pthlem  29741  crctcshwlkn0  29799  wwlksnextinj  29877  wwlksnextproplem2  29888  wwlksnextproplem3  29889  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwwlkf1  30029  clwwlknwwlksnb  30035  clwwlkext2edg  30036  clwwlknonex2lem2  30088  frgr3vlem1  30253  3vfriswmgrlem  30257  vdgn1frgrv2  30276  frgrwopreglem5  30301  frgrwopreglem5ALT  30302  mdexchi  32315  atomli  32362  mdsymlem5  32387  sumdmdlem  32398  dfimafnf  32618  prmidlc  33413  bnj517  34897  bnj1118  34996  mclsind  35614  dfon2lem6  35830  btwnconn1lem11  36141  finminlem  36362  isbasisrelowllem1  37399  isbasisrelowllem2  37400  poimirlem27  37697  itg2addnc  37724  rngoueqz  37990  dmncan1  38126  disjlem19  38909  lshpdisj  39096  2at0mat0  39634  llncvrlpln2  39666  lplncvrlvol2  39724  lhpexle2lem  40118  cdlemk33N  41018  cdlemk34  41019  sn-sup3d  42595  eldioph2  42865  cantnfresb  43427  gneispacess2  44249  sge0iunmpt  46526  funressnfv  47153  dfaimafn  47275  otiunsndisjX  47389  elfz2z  47425  iccelpart  47543  icceuelpart  47546  fargshiftfva  47553  sprsymrelfo  47607  sbcpr  47631  bgoldbtbndlem4  47918  grimcnv  47998  grimco  47999  clnbgrgrim  48044  uspgrlimlem4  48101  grlicsym  48123  grlictr  48125  pgnbgreunbgrlem3  48228  pgnbgreunbgrlem6  48234  snlindsntor  48582  ldepspr  48584  nn0sumshdiglemB  48731