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  655  3imp  1111  reusv3  5347  otiunsndisj  5474  pwssun  5523  ordelord  6345  tz7.7  6349  dfimafn  6902  funimass4  6904  funimass3  7006  isomin  7292  isopolem  7300  onint  7744  limsssuc  7801  tfindsg  7812  findsg  7848  suppfnss  8139  smores2  8294  tfrlem9  8324  tz7.49  8384  oecl  8472  oaordi  8481  oaass  8496  omordi  8501  odi  8514  oen0  8522  nnaordi  8554  nnmordi  8567  domunfican  9232  dfac5  10051  cofsmo  10191  cfcoflem  10194  zorn2lem7  10424  tskwun  10707  mulcanpi  10823  ltexprlem7  10965  sup3  12113  elnnz  12534  nzadd  12575  irradd  12923  irrmul  12924  uzsubsubfz  13500  fzo1fzo0n0  13670  elincfzoext  13678  elfzonelfzo  13724  uzindi  13944  ssnn0fi  13947  sqlecan  14171  swrdnd2  14618  swrdwrdsymb  14625  wrd2ind  14685  repswccat  14748  cshwlen  14761  cshwidxmod  14765  2cshwcshw  14787  wrdl3s3  14924  lcmfunsnlem1  16606  coprmprod  16630  unbenlem  16879  infpnlem1  16881  prmgaplem7  17028  iscatd  17639  dirtr  18568  telgsums  19968  zrtermorngc  20620  zrtermoringc  20652  psgndiflemA  21581  isphld  21634  gsummoncoe1  22273  gsummatr01lem3  22622  cpmatmcllem  22683  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  cayleyhamilton1  22857  tgcl  22934  neindisj2  23088  2ndcdisj  23421  fgcl  23843  rnelfm  23918  alexsubALTlem3  24014  2sqreultlem  27410  2sqreunnltlem  27413  elnnzs  28393  usgrexmpledg  29331  cusgrsize  29523  uspgr2wlkeqi  29716  usgr2wlkneq  29824  usgr2pthlem  29831  crctcshwlkn0  29889  wwlksnextinj  29967  wwlksnextproplem2  29978  wwlksnextproplem3  29979  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwlkf1  30119  clwwlknwwlksnb  30125  clwwlkext2edg  30126  clwwlknonex2lem2  30178  frgr3vlem1  30343  3vfriswmgrlem  30347  vdgn1frgrv2  30366  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  mdexchi  32406  atomli  32453  mdsymlem5  32478  sumdmdlem  32489  dfimafnf  32709  prmidlc  33508  bnj517  35027  bnj1118  35126  mclsind  35752  dfon2lem6  35968  btwnconn1lem11  36279  finminlem  36500  isbasisrelowllem1  37671  isbasisrelowllem2  37672  poimirlem27  37968  itg2addnc  37995  rngoueqz  38261  dmncan1  38397  disjlem19  39225  lshpdisj  39433  2at0mat0  39971  llncvrlpln2  40003  lplncvrlvol2  40061  pmaple  40207  lhpexle2lem  40455  cdlemk33N  41355  cdlemk34  41356  sn-sup3d  42937  eldioph2  43194  cantnfresb  43752  gneispacess2  44573  sge0iunmpt  46846  funressnfv  47491  dfaimafn  47613  otiunsndisjX  47727  elfz2z  47763  iccelpart  47893  icceuelpart  47896  fargshiftfva  47903  sprsymrelfo  47957  sbcpr  47981  bgoldbtbndlem4  48284  grimcnv  48364  grimco  48365  clnbgrgrim  48410  uspgrlimlem4  48467  grlicsym  48489  grlictr  48491  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  snlindsntor  48947  ldepspr  48949  nn0sumshdiglemB  49096