Theorem imp31 448

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

Hypothesis

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

Assertion

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

Proof of Theorem imp31

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  imp41  619  imp5d  625  impl  650  anassrs  680  an31s  848  3imp  1256  3expa  1265  reusv3  4876  otiunsndisj  4980  pwssun  5020  fri  5076  predpo  5698  ordelord  5745  tz7.7  5749  dfimafn  6245  funimass4  6247  funimass3  6333  isomin  6587  isopolem  6595  onint  6995  limsssuc  7050  tfindsg  7060  findsg  7093  suppfnss  7320  smores2  7451  tfrlem9  7481  tz7.49  7540  oecl  7617  oaordi  7626  oaass  7641  omordi  7646  odi  7659  oen0  7666  nnaordi  7698  nnmordi  7711  php3  8146  domunfican  8233  dfac5  8951  cofsmo  9091  cfcoflem  9094  zorn2lem7  9324  tskwun  9606  mulcanpi  9722  ltexprlem7  9864  sup3  10980  elnnz  11387  nzadd  11425  irradd  11812  irrmul  11813  uzsubsubfz  12363  fzo1fzo0n0  12518  elincfzoext  12525  elfzonelfzo  12570  uzindi  12781  ssnn0fi  12784  sqlecan  12971  wrd2ind  13477  repswccat  13532  cshwlen  13545  cshwidxmod  13549  2cshwcshw  13571  wrdl3s3  13705  lcmfunsnlem1  15350  lcmfdvdsb  15356  coprmprod  15375  unbenlem  15612  infpnlem1  15614  prmgaplem7  15761  iscatd  16334  initoeu1  16661  termoeu1  16668  dirtr  17236  telgsums  18390  psrbaglefi  19372  gsummoncoe1  19674  psgndiflemA  19947  isphld  19999  gsummatr01lem3  20463  cpmatmcllem  20523  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  cayleyhamilton1  20697  tgcl  20773  neindisj2  20927  2ndcdisj  21259  fgcl  21682  rnelfm  21757  alexsubALTlem3  21853  usgrexmpledg  26154  cusgrsize  26350  uspgr2wlkeqi  26544  usgr2wlkneq  26652  usgr2pthlem  26659  crctcshwlkn0  26713  wwlksnextinj  26794  wwlksnextproplem2  26805  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksf1  26917  clwwlksext2edg  26923  frgr3vlem1  27137  3vfriswmgrlem  27141  vdgn1frgrv2  27160  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  numclwwlkovf2exlem2  27212  mdexchi  29194  atomli  29241  mdsymlem5  29266  sumdmdlem  29277  dfimafnf  29436  bnj517  30955  bnj1118  31052  mclsind  31467  dfon2lem6  31693  btwnconn1lem11  32204  finminlem  32312  bj-snmoore  33068  isbasisrelowllem1  33203  isbasisrelowllem2  33204  poimirlem27  33436  itg2addnc  33464  rngoueqz  33739  dmncan1  33875  lshpdisj  34274  2at0mat0  34811  llncvrlpln2  34843  lplncvrlvol2  34901  lhpexle2lem  35295  cdlemk33N  36197  cdlemk34  36198  eldioph2  37325  gneispacess2  38444  sge0iunmpt  40635  funressnfv  41208  dfaimafn  41245  otiunsndisjX  41298  elfz2z  41325  iccelpart  41369  icceuelpart  41372  fargshiftfva  41379  bgoldbtbndlem4  41696  sprsymrelfo  41747  zrtermorngc  42001  zrtermoringc  42070  snlindsntor  42260  ldepspr  42262  nn0sumshdiglemB  42414