Theorem imp31 420

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imp41  428  imp5d  442  impl  458  anassrs  470  an31s  652  3imp  1107  reusv3  5306  otiunsndisj  5410  pwssun  5456  fri  5517  predpo  6166  ordelord  6213  tz7.7  6217  dfimafn  6728  funimass4  6730  funimass3  6824  isomin  7090  isopolem  7098  onint  7510  limsssuc  7565  tfindsg  7575  findsg  7609  suppfnss  7855  smores2  7991  tfrlem9  8021  tz7.49  8081  oecl  8162  oaordi  8172  oaass  8187  omordi  8192  odi  8205  oen0  8212  nnaordi  8244  nnmordi  8257  php3  8703  domunfican  8791  dfac5  9554  cofsmo  9691  cfcoflem  9694  zorn2lem7  9924  tskwun  10206  mulcanpi  10322  ltexprlem7  10464  sup3  11598  elnnz  11992  nzadd  12031  irradd  12373  irrmul  12374  uzsubsubfz  12930  fzo1fzo0n0  13089  elincfzoext  13096  elfzonelfzo  13140  uzindi  13351  ssnn0fi  13354  sqlecan  13572  swrdnd2  14017  swrdwrdsymb  14024  wrd2ind  14085  repswccat  14148  cshwlen  14161  cshwidxmod  14165  2cshwcshw  14187  wrdl3s3  14326  lcmfunsnlem1  15981  coprmprod  16005  unbenlem  16244  infpnlem1  16246  prmgaplem7  16393  iscatd  16944  dirtr  17846  telgsums  19113  psrbaglefi  20152  gsummoncoe1  20472  psgndiflemA  20745  isphld  20798  gsummatr01lem3  21266  cpmatmcllem  21326  mp2pm2mplem4  21417  chfacfisf  21462  chfacfisfcpmat  21463  cayleyhamilton1  21500  tgcl  21577  neindisj2  21731  2ndcdisj  22064  fgcl  22486  rnelfm  22561  alexsubALTlem3  22657  2sqreultlem  26023  2sqreunnltlem  26026  usgrexmpledg  27044  cusgrsize  27236  uspgr2wlkeqi  27429  usgr2wlkneq  27537  usgr2pthlem  27544  crctcshwlkn0  27599  wwlksnextinj  27677  wwlksnextproplem2  27689  wwlksnextproplem3  27690  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwwlkf1  27828  clwwlknwwlksnb  27834  clwwlkext2edg  27835  clwwlknonex2lem2  27887  frgr3vlem1  28052  3vfriswmgrlem  28056  vdgn1frgrv2  28075  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  mdexchi  30112  atomli  30159  mdsymlem5  30184  sumdmdlem  30195  dfimafnf  30381  prmidlc  30964  bnj517  32157  bnj1118  32256  mclsind  32817  dfon2lem6  33033  btwnconn1lem11  33558  finminlem  33666  isbasisrelowllem1  34639  isbasisrelowllem2  34640  poimirlem27  34934  itg2addnc  34961  rngoueqz  35233  dmncan1  35369  lshpdisj  36138  2at0mat0  36676  llncvrlpln2  36708  lplncvrlvol2  36766  lhpexle2lem  37160  cdlemk33N  38060  cdlemk34  38061  eldioph2  39379  gneispacess2  40516  sge0iunmpt  42720  funressnfv  43298  dfaimafn  43384  otiunsndisjX  43498  elfz2z  43535  iccelpart  43613  icceuelpart  43616  fargshiftfva  43623  sprsymrelfo  43679  sbcpr  43703  bgoldbtbndlem4  43993  isomuspgrlem1  44012  isomuspgrlem2b  44014  isomuspgrlem2d  44016  zrtermorngc  44292  zrtermoringc  44361  snlindsntor  44546  ldepspr  44548  nn0sumshdiglemB  44700