Theorem imp31 421

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 410	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 410	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  imp41  429  imp5d  443  impl  459  anassrs  471  an31s  664  3imp  1123  reusv3  5362  otiunsndisj  5489  pwssun  5539  ordelord  6368  tz7.7  6372  dfimafn  6929  funimass4  6931  funimass3  7035  isomin  7321  isopolem  7329  onint  7773  limsssuc  7830  tfindsg  7841  findsg  7878  suppfnss  8169  smores2  8325  tfrlem9  8356  tz7.49  8416  oecl  8506  oaordi  8515  oaass  8530  omordi  8535  odi  8548  oen0  8556  nnaordi  8588  nnmordi  8601  domunfican  9266  dfac5  10085  cofsmo  10226  cfcoflem  10229  zorn2lem7  10459  tskwun  10742  mulcanpi  10858  ltexprlem7  11000  sup3  12149  elnnz  12578  nzadd  12619  irradd  12974  irrmul  12975  uzsubsubfz  13551  fzo1fzo0n0  13721  elincfzoext  13729  elfzonelfzo  13775  uzindi  13995  ssnn0fi  13998  sqlecan  14222  swrdnd2  14669  swrdwrdsymb  14676  wrd2ind  14736  repswccat  14799  cshwlen  14812  cshwidxmod  14816  2cshwcshw  14838  wrdl3s3  14975  lcmfunsnlem1  16671  coprmprod  16695  unbenlem  16944  infpnlem1  16946  prmgaplem7  17093  iscatd  17705  dirtr  18634  telgsums  20033  zrtermorngc  20693  zrtermoringc  20725  psgndiflemA  21653  isphld  21706  gsummoncoe1  22371  gsummatr01lem3  22717  cpmatmcllem  22778  mp2pm2mplem4  22869  chfacfisf  22914  chfacfisfcpmat  22915  cayleyhamilton1  22952  tgcl  23029  neindisj2  23183  2ndcdisj  23516  fgcl  23938  rnelfm  24013  alexsubALTlem3  24109  2sqreultlem  27511  2sqreunnltlem  27514  elnnzs  28494  usgrexmpledg  29463  cusgrsize  29655  uspgr2wlkeqi  29848  usgr2wlkneq  29956  usgr2pthlem  29963  crctcshwlkn0  30021  wwlksnextinj  30099  wwlksnextproplem2  30110  wwlksnextproplem3  30111  clwlkclwwlklem2a  30200  clwlkclwwlklem2  30202  clwwlkf1  30251  clwwlknwwlksnb  30257  clwwlkext2edg  30258  clwwlknonex2lem2  30310  frgr3vlem1  30475  3vfriswmgrlem  30479  vdgn1frgrv2  30498  frgrwopreglem5  30523  frgrwopreglem5ALT  30524  mdexchi  32538  atomli  32585  mdsymlem5  32610  sumdmdlem  32621  dfimafnf  32838  prmidlc  33634  bnj517  35180  bnj1118  35279  mclsind  35920  dfon2lem6  36136  btwnconn1lem11  36447  finminlem  36678  isbasisrelowllem1  37849  isbasisrelowllem2  37850  poimirlem27  38146  itg2addnc  38173  rngoueqz  38439  dmncan1  38575  disjlem19  39403  lshpdisj  39611  2at0mat0  40149  llncvrlpln2  40181  lplncvrlvol2  40239  pmaple  40385  lhpexle2lem  40633  cdlemk33N  41533  cdlemk34  41534  sn-sup3d  43114  eldioph2  43343  cantnfresb  43901  gneispacess2  44722  sge0iunmpt  46992  funressnfv  47637  dfaimafn  47759  otiunsndisjX  47873  elfz2z  47909  iccelpart  48039  icceuelpart  48042  fargshiftfva  48049  sprsymrelfo  48103  sbcpr  48127  bgoldbtbndlem4  48430  grimcnv  48510  grimco  48511  clnbgrgrim  48556  uspgrlimlem4  48613  grlicsym  48635  grlictr  48637  pgnbgreunbgrlem3  48740  pgnbgreunbgrlem6  48746  snlindsntor  49093  ldepspr  49095  nn0sumshdiglemB  49242