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  653  3imp  1111  reusv3  5423  otiunsndisj  5539  pwssun  5590  friOLD  5658  ordelord  6417  tz7.7  6421  dfimafn  6984  funimass4  6986  funimass3  7087  isomin  7373  isopolem  7381  onint  7826  limsssuc  7887  tfindsg  7898  findsg  7937  suppfnss  8230  smores2  8410  tfrlem9  8441  tz7.49  8501  oecl  8593  oaordi  8602  oaass  8617  omordi  8622  odi  8635  oen0  8642  nnaordi  8674  nnmordi  8687  php3OLD  9287  domunfican  9389  dfac5  10198  cofsmo  10338  cfcoflem  10341  zorn2lem7  10571  tskwun  10853  mulcanpi  10969  ltexprlem7  11111  sup3  12252  elnnz  12649  nzadd  12691  irradd  13038  irrmul  13039  uzsubsubfz  13606  fzo1fzo0n0  13767  elincfzoext  13774  elfzonelfzo  13819  uzindi  14033  ssnn0fi  14036  sqlecan  14258  swrdnd2  14703  swrdwrdsymb  14710  wrd2ind  14771  repswccat  14834  cshwlen  14847  cshwidxmod  14851  2cshwcshw  14874  wrdl3s3  15011  lcmfunsnlem1  16684  coprmprod  16708  unbenlem  16955  infpnlem1  16957  prmgaplem7  17104  iscatd  17731  dirtr  18672  telgsums  20035  zrtermorngc  20665  zrtermoringc  20697  psgndiflemA  21642  isphld  21695  gsummoncoe1  22333  gsummatr01lem3  22684  cpmatmcllem  22745  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  cayleyhamilton1  22919  tgcl  22997  neindisj2  23152  2ndcdisj  23485  fgcl  23907  rnelfm  23982  alexsubALTlem3  24078  2sqreultlem  27509  2sqreunnltlem  27512  elnnzs  28405  usgrexmpledg  29297  cusgrsize  29490  uspgr2wlkeqi  29684  usgr2wlkneq  29792  usgr2pthlem  29799  crctcshwlkn0  29854  wwlksnextinj  29932  wwlksnextproplem2  29943  wwlksnextproplem3  29944  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwwlkf1  30081  clwwlknwwlksnb  30087  clwwlkext2edg  30088  clwwlknonex2lem2  30140  frgr3vlem1  30305  3vfriswmgrlem  30309  vdgn1frgrv2  30328  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  mdexchi  32367  atomli  32414  mdsymlem5  32439  sumdmdlem  32450  dfimafnf  32655  prmidlc  33441  bnj517  34861  bnj1118  34960  mclsind  35538  dfon2lem6  35752  btwnconn1lem11  36061  finminlem  36284  isbasisrelowllem1  37321  isbasisrelowllem2  37322  poimirlem27  37607  itg2addnc  37634  rngoueqz  37900  dmncan1  38036  disjlem19  38757  lshpdisj  38943  2at0mat0  39482  llncvrlpln2  39514  lplncvrlvol2  39572  lhpexle2lem  39966  cdlemk33N  40866  cdlemk34  40867  sn-sup3d  42448  eldioph2  42718  cantnfresb  43286  gneispacess2  44108  sge0iunmpt  46339  funressnfv  46958  dfaimafn  47080  otiunsndisjX  47194  elfz2z  47230  iccelpart  47307  icceuelpart  47310  fargshiftfva  47317  sprsymrelfo  47371  sbcpr  47395  bgoldbtbndlem4  47682  grimcnv  47763  grimco  47764  clnbgrgrim  47786  uspgrlimlem4  47815  grlicsym  47830  grlictr  47832  snlindsntor  48200  ldepspr  48202  nn0sumshdiglemB  48354