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  5375  otiunsndisj  5495  pwssun  5545  friOLD  5612  ordelord  6374  tz7.7  6378  dfimafn  6940  funimass4  6942  funimass3  7043  isomin  7329  isopolem  7337  onint  7782  limsssuc  7843  tfindsg  7854  findsg  7891  suppfnss  8186  smores2  8366  tfrlem9  8397  tz7.49  8457  oecl  8547  oaordi  8556  oaass  8571  omordi  8576  odi  8589  oen0  8596  nnaordi  8628  nnmordi  8641  php3OLD  9231  domunfican  9331  dfac5  10141  cofsmo  10281  cfcoflem  10284  zorn2lem7  10514  tskwun  10796  mulcanpi  10912  ltexprlem7  11054  sup3  12197  elnnz  12596  nzadd  12638  irradd  12987  irrmul  12988  uzsubsubfz  13561  fzo1fzo0n0  13729  elincfzoext  13737  elfzonelfzo  13783  uzindi  13998  ssnn0fi  14001  sqlecan  14225  swrdnd2  14671  swrdwrdsymb  14678  wrd2ind  14739  repswccat  14802  cshwlen  14815  cshwidxmod  14819  2cshwcshw  14842  wrdl3s3  14979  lcmfunsnlem1  16654  coprmprod  16678  unbenlem  16926  infpnlem1  16928  prmgaplem7  17075  iscatd  17683  dirtr  18610  telgsums  19972  zrtermorngc  20601  zrtermoringc  20633  psgndiflemA  21559  isphld  21612  gsummoncoe1  22244  gsummatr01lem3  22593  cpmatmcllem  22654  mp2pm2mplem4  22745  chfacfisf  22790  chfacfisfcpmat  22791  cayleyhamilton1  22828  tgcl  22905  neindisj2  23059  2ndcdisj  23392  fgcl  23814  rnelfm  23889  alexsubALTlem3  23985  2sqreultlem  27408  2sqreunnltlem  27411  elnnzs  28304  usgrexmpledg  29187  cusgrsize  29380  uspgr2wlkeqi  29574  usgr2wlkneq  29684  usgr2pthlem  29691  crctcshwlkn0  29749  wwlksnextinj  29827  wwlksnextproplem2  29838  wwlksnextproplem3  29839  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwwlkf1  29976  clwwlknwwlksnb  29982  clwwlkext2edg  29983  clwwlknonex2lem2  30035  frgr3vlem1  30200  3vfriswmgrlem  30204  vdgn1frgrv2  30223  frgrwopreglem5  30248  frgrwopreglem5ALT  30249  mdexchi  32262  atomli  32309  mdsymlem5  32334  sumdmdlem  32345  dfimafnf  32560  prmidlc  33409  bnj517  34862  bnj1118  34961  mclsind  35538  dfon2lem6  35752  btwnconn1lem11  36061  finminlem  36282  isbasisrelowllem1  37319  isbasisrelowllem2  37320  poimirlem27  37617  itg2addnc  37644  rngoueqz  37910  dmncan1  38046  disjlem19  38765  lshpdisj  38951  2at0mat0  39490  llncvrlpln2  39522  lplncvrlvol2  39580  lhpexle2lem  39974  cdlemk33N  40874  cdlemk34  40875  sn-sup3d  42462  eldioph2  42732  cantnfresb  43295  gneispacess2  44117  sge0iunmpt  46395  funressnfv  47020  dfaimafn  47142  otiunsndisjX  47256  elfz2z  47292  iccelpart  47395  icceuelpart  47398  fargshiftfva  47405  sprsymrelfo  47459  sbcpr  47483  bgoldbtbndlem4  47770  grimcnv  47849  grimco  47850  clnbgrgrim  47895  uspgrlimlem4  47951  grlicsym  47966  grlictr  47968  snlindsntor  48395  ldepspr  48397  nn0sumshdiglemB  48548