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  5305  otiunsndisj  5409  pwssun  5455  fri  5516  predpo  6165  ordelord  6212  tz7.7  6216  dfimafn  6727  funimass4  6729  funimass3  6823  isomin  7089  isopolem  7097  onint  7509  limsssuc  7564  tfindsg  7574  findsg  7608  suppfnss  7854  smores2  7990  tfrlem9  8020  tz7.49  8080  oecl  8161  oaordi  8171  oaass  8186  omordi  8191  odi  8204  oen0  8211  nnaordi  8243  nnmordi  8256  php3  8702  domunfican  8790  dfac5  9553  cofsmo  9690  cfcoflem  9693  zorn2lem7  9923  tskwun  10205  mulcanpi  10321  ltexprlem7  10463  sup3  11597  elnnz  11990  nzadd  12029  irradd  12371  irrmul  12372  uzsubsubfz  12928  fzo1fzo0n0  13087  elincfzoext  13094  elfzonelfzo  13138  uzindi  13349  ssnn0fi  13352  sqlecan  13570  swrdnd2  14016  swrdwrdsymb  14023  wrd2ind  14084  repswccat  14147  cshwlen  14160  cshwidxmod  14164  2cshwcshw  14186  wrdl3s3  14325  lcmfunsnlem1  15980  coprmprod  16004  unbenlem  16243  infpnlem1  16245  prmgaplem7  16392  iscatd  16943  dirtr  17845  telgsums  19112  psrbaglefi  20151  gsummoncoe1  20471  psgndiflemA  20744  isphld  20797  gsummatr01lem3  21265  cpmatmcllem  21325  mp2pm2mplem4  21416  chfacfisf  21461  chfacfisfcpmat  21462  cayleyhamilton1  21499  tgcl  21576  neindisj2  21730  2ndcdisj  22063  fgcl  22485  rnelfm  22560  alexsubALTlem3  22656  2sqreultlem  26022  2sqreunnltlem  26025  usgrexmpledg  27043  cusgrsize  27235  uspgr2wlkeqi  27428  usgr2wlkneq  27536  usgr2pthlem  27543  crctcshwlkn0  27598  wwlksnextinj  27676  wwlksnextproplem2  27688  wwlksnextproplem3  27689  clwlkclwwlklem2a  27775  clwlkclwwlklem2  27777  clwwlkf1  27827  clwwlknwwlksnb  27833  clwwlkext2edg  27834  clwwlknonex2lem2  27886  frgr3vlem1  28051  3vfriswmgrlem  28055  vdgn1frgrv2  28074  frgrwopreglem5  28099  frgrwopreglem5ALT  28100  mdexchi  30111  atomli  30158  mdsymlem5  30183  sumdmdlem  30194  dfimafnf  30380  prmidlc  30964  bnj517  32157  bnj1118  32256  mclsind  32817  dfon2lem6  33033  btwnconn1lem11  33558  finminlem  33666  isbasisrelowllem1  34635  isbasisrelowllem2  34636  poimirlem27  34918  itg2addnc  34945  rngoueqz  35217  dmncan1  35353  lshpdisj  36122  2at0mat0  36660  llncvrlpln2  36692  lplncvrlvol2  36750  lhpexle2lem  37144  cdlemk33N  38044  cdlemk34  38045  eldioph2  39357  gneispacess2  40494  sge0iunmpt  42699  funressnfv  43277  dfaimafn  43363  otiunsndisjX  43477  elfz2z  43514  iccelpart  43592  icceuelpart  43595  fargshiftfva  43602  sprsymrelfo  43658  sbcpr  43682  bgoldbtbndlem4  43972  isomuspgrlem1  43991  isomuspgrlem2b  43993  isomuspgrlem2d  43995  zrtermorngc  44271  zrtermoringc  44340  snlindsntor  44525  ldepspr  44527  nn0sumshdiglemB  44679