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  5360  otiunsndisj  5480  pwssun  5530  ordelord  6354  tz7.7  6358  dfimafn  6923  funimass4  6925  funimass3  7026  isomin  7312  isopolem  7320  onint  7766  limsssuc  7826  tfindsg  7837  findsg  7873  suppfnss  8168  smores2  8323  tfrlem9  8353  tz7.49  8413  oecl  8501  oaordi  8510  oaass  8525  omordi  8530  odi  8543  oen0  8550  nnaordi  8582  nnmordi  8595  domunfican  9272  dfac5  10082  cofsmo  10222  cfcoflem  10225  zorn2lem7  10455  tskwun  10737  mulcanpi  10853  ltexprlem7  10995  sup3  12140  elnnz  12539  nzadd  12581  irradd  12932  irrmul  12933  uzsubsubfz  13507  fzo1fzo0n0  13676  elincfzoext  13684  elfzonelfzo  13730  uzindi  13947  ssnn0fi  13950  sqlecan  14174  swrdnd2  14620  swrdwrdsymb  14627  wrd2ind  14688  repswccat  14751  cshwlen  14764  cshwidxmod  14768  2cshwcshw  14791  wrdl3s3  14928  lcmfunsnlem1  16607  coprmprod  16631  unbenlem  16879  infpnlem1  16881  prmgaplem7  17028  iscatd  17634  dirtr  18561  telgsums  19923  zrtermorngc  20552  zrtermoringc  20584  psgndiflemA  21510  isphld  21563  gsummoncoe1  22195  gsummatr01lem3  22544  cpmatmcllem  22605  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  cayleyhamilton1  22779  tgcl  22856  neindisj2  23010  2ndcdisj  23343  fgcl  23765  rnelfm  23840  alexsubALTlem3  23936  2sqreultlem  27358  2sqreunnltlem  27361  elnnzs  28289  usgrexmpledg  29189  cusgrsize  29382  uspgr2wlkeqi  29576  usgr2wlkneq  29686  usgr2pthlem  29693  crctcshwlkn0  29751  wwlksnextinj  29829  wwlksnextproplem2  29840  wwlksnextproplem3  29841  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwwlkf1  29978  clwwlknwwlksnb  29984  clwwlkext2edg  29985  clwwlknonex2lem2  30037  frgr3vlem1  30202  3vfriswmgrlem  30206  vdgn1frgrv2  30225  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  mdexchi  32264  atomli  32311  mdsymlem5  32336  sumdmdlem  32347  dfimafnf  32560  prmidlc  33419  bnj517  34875  bnj1118  34974  mclsind  35557  dfon2lem6  35776  btwnconn1lem11  36085  finminlem  36306  isbasisrelowllem1  37343  isbasisrelowllem2  37344  poimirlem27  37641  itg2addnc  37668  rngoueqz  37934  dmncan1  38070  disjlem19  38793  lshpdisj  38980  2at0mat0  39519  llncvrlpln2  39551  lplncvrlvol2  39609  lhpexle2lem  40003  cdlemk33N  40903  cdlemk34  40904  sn-sup3d  42480  eldioph2  42750  cantnfresb  43313  gneispacess2  44135  sge0iunmpt  46416  funressnfv  47044  dfaimafn  47166  otiunsndisjX  47280  elfz2z  47316  iccelpart  47434  icceuelpart  47437  fargshiftfva  47444  sprsymrelfo  47498  sbcpr  47522  bgoldbtbndlem4  47809  grimcnv  47888  grimco  47889  clnbgrgrim  47934  uspgrlimlem4  47990  grlicsym  48005  grlictr  48007  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  snlindsntor  48460  ldepspr  48462  nn0sumshdiglemB  48609