Theorem imp31 418

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  imp41  426  imp5d  440  impl  456  anassrs  468  an31s  651  3imp  1110  reusv3  5329  otiunsndisj  5435  pwssun  5486  friOLD  5551  ordelord  6292  tz7.7  6296  dfimafn  6841  funimass4  6843  funimass3  6940  isomin  7217  isopolem  7225  onint  7649  limsssuc  7706  tfindsg  7716  findsg  7755  suppfnss  8014  smores2  8194  tfrlem9  8225  tz7.49  8285  oecl  8376  oaordi  8386  oaass  8401  omordi  8406  odi  8419  oen0  8426  nnaordi  8458  nnmordi  8471  php3OLD  9016  domunfican  9096  dfac5  9893  cofsmo  10034  cfcoflem  10037  zorn2lem7  10267  tskwun  10549  mulcanpi  10665  ltexprlem7  10807  sup3  11941  elnnz  12338  nzadd  12377  irradd  12722  irrmul  12723  uzsubsubfz  13287  fzo1fzo0n0  13447  elincfzoext  13454  elfzonelfzo  13498  uzindi  13711  ssnn0fi  13714  sqlecan  13934  swrdnd2  14377  swrdwrdsymb  14384  wrd2ind  14445  repswccat  14508  cshwlen  14521  cshwidxmod  14525  2cshwcshw  14547  wrdl3s3  14686  lcmfunsnlem1  16351  coprmprod  16375  unbenlem  16618  infpnlem1  16620  prmgaplem7  16767  iscatd  17391  dirtr  18329  telgsums  19603  psgndiflemA  20815  isphld  20868  psrbaglefiOLD  21145  gsummoncoe1  21484  gsummatr01lem3  21815  cpmatmcllem  21876  mp2pm2mplem4  21967  chfacfisf  22012  chfacfisfcpmat  22013  cayleyhamilton1  22050  tgcl  22128  neindisj2  22283  2ndcdisj  22616  fgcl  23038  rnelfm  23113  alexsubALTlem3  23209  2sqreultlem  26604  2sqreunnltlem  26607  usgrexmpledg  27638  cusgrsize  27830  uspgr2wlkeqi  28024  usgr2wlkneq  28133  usgr2pthlem  28140  crctcshwlkn0  28195  wwlksnextinj  28273  wwlksnextproplem2  28284  wwlksnextproplem3  28285  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwwlkf1  28422  clwwlknwwlksnb  28428  clwwlkext2edg  28429  clwwlknonex2lem2  28481  frgr3vlem1  28646  3vfriswmgrlem  28650  vdgn1frgrv2  28669  frgrwopreglem5  28694  frgrwopreglem5ALT  28695  mdexchi  30706  atomli  30753  mdsymlem5  30778  sumdmdlem  30789  dfimafnf  30980  prmidlc  31633  bnj517  32874  bnj1118  32973  mclsind  33541  dfon2lem6  33773  btwnconn1lem11  34408  finminlem  34516  isbasisrelowllem1  35535  isbasisrelowllem2  35536  poimirlem27  35813  itg2addnc  35840  rngoueqz  36107  dmncan1  36243  lshpdisj  37008  2at0mat0  37546  llncvrlpln2  37578  lplncvrlvol2  37636  lhpexle2lem  38030  cdlemk33N  38930  cdlemk34  38931  eldioph2  40591  gneispacess2  41763  sge0iunmpt  43963  funressnfv  44548  dfaimafn  44668  otiunsndisjX  44782  elfz2z  44818  iccelpart  44896  icceuelpart  44899  fargshiftfva  44906  sprsymrelfo  44960  sbcpr  44984  bgoldbtbndlem4  45271  isomuspgrlem1  45290  isomuspgrlem2b  45292  isomuspgrlem2d  45294  zrtermorngc  45570  zrtermoringc  45639  snlindsntor  45823  ldepspr  45825  nn0sumshdiglemB  45977