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  5344  otiunsndisj  5463  pwssun  5511  ordelord  6329  tz7.7  6333  dfimafn  6885  funimass4  6887  funimass3  6988  isomin  7274  isopolem  7282  onint  7726  limsssuc  7783  tfindsg  7794  findsg  7830  suppfnss  8122  smores2  8277  tfrlem9  8307  tz7.49  8367  oecl  8455  oaordi  8464  oaass  8479  omordi  8484  odi  8497  oen0  8504  nnaordi  8536  nnmordi  8549  domunfican  9211  dfac5  10023  cofsmo  10163  cfcoflem  10166  zorn2lem7  10396  tskwun  10678  mulcanpi  10794  ltexprlem7  10936  sup3  12082  elnnz  12481  nzadd  12523  irradd  12874  irrmul  12875  uzsubsubfz  13449  fzo1fzo0n0  13618  elincfzoext  13626  elfzonelfzo  13672  uzindi  13889  ssnn0fi  13892  sqlecan  14116  swrdnd2  14562  swrdwrdsymb  14569  wrd2ind  14629  repswccat  14692  cshwlen  14705  cshwidxmod  14709  2cshwcshw  14732  wrdl3s3  14869  lcmfunsnlem1  16548  coprmprod  16572  unbenlem  16820  infpnlem1  16822  prmgaplem7  16969  iscatd  17579  dirtr  18508  telgsums  19872  zrtermorngc  20528  zrtermoringc  20560  psgndiflemA  21508  isphld  21561  gsummoncoe1  22193  gsummatr01lem3  22542  cpmatmcllem  22603  mp2pm2mplem4  22694  chfacfisf  22739  chfacfisfcpmat  22740  cayleyhamilton1  22777  tgcl  22854  neindisj2  23008  2ndcdisj  23341  fgcl  23763  rnelfm  23838  alexsubALTlem3  23934  2sqreultlem  27356  2sqreunnltlem  27359  elnnzs  28294  usgrexmpledg  29207  cusgrsize  29400  uspgr2wlkeqi  29593  usgr2wlkneq  29701  usgr2pthlem  29708  crctcshwlkn0  29766  wwlksnextinj  29844  wwlksnextproplem2  29855  wwlksnextproplem3  29856  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwwlkf1  29993  clwwlknwwlksnb  29999  clwwlkext2edg  30000  clwwlknonex2lem2  30052  frgr3vlem1  30217  3vfriswmgrlem  30221  vdgn1frgrv2  30240  frgrwopreglem5  30265  frgrwopreglem5ALT  30266  mdexchi  32279  atomli  32326  mdsymlem5  32351  sumdmdlem  32362  dfimafnf  32579  prmidlc  33385  bnj517  34852  bnj1118  34951  mclsind  35547  dfon2lem6  35766  btwnconn1lem11  36075  finminlem  36296  isbasisrelowllem1  37333  isbasisrelowllem2  37334  poimirlem27  37631  itg2addnc  37658  rngoueqz  37924  dmncan1  38060  disjlem19  38783  lshpdisj  38970  2at0mat0  39508  llncvrlpln2  39540  lplncvrlvol2  39598  lhpexle2lem  39992  cdlemk33N  40892  cdlemk34  40893  sn-sup3d  42469  eldioph2  42739  cantnfresb  43301  gneispacess2  44123  sge0iunmpt  46403  funressnfv  47031  dfaimafn  47153  otiunsndisjX  47267  elfz2z  47303  iccelpart  47421  icceuelpart  47424  fargshiftfva  47431  sprsymrelfo  47485  sbcpr  47509  bgoldbtbndlem4  47796  grimcnv  47876  grimco  47877  clnbgrgrim  47922  uspgrlimlem4  47979  grlicsym  48001  grlictr  48003  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112  snlindsntor  48460  ldepspr  48462  nn0sumshdiglemB  48609