Theorem imp31 422

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp41  430  imp5d  444  impl  460  anassrs  472  an31s  666  3imp  1128  reusv3  5376  otiunsndisj  5503  pwssun  5553  ordelord  6382  tz7.7  6386  dfimafn  6943  funimass4  6945  funimass3  7049  isomin  7335  isopolem  7343  onint  7785  limsssuc  7842  tfindsg  7853  findsg  7890  suppfnss  8181  smores2  8337  tfrlem9  8368  tz7.49  8428  oecl  8518  oaordi  8527  oaass  8542  omordi  8547  odi  8560  oen0  8568  nnaordi  8600  nnmordi  8613  domunfican  9277  dfac5  10108  cofsmo  10248  cfcoflem  10251  zorn2lem7  10481  tskwun  10764  mulcanpi  10880  ltexprlem7  11022  sup3  12167  elnnz  12596  nzadd  12637  irradd  12992  irrmul  12993  uzsubsubfz  13570  fzo1fzo0n0  13740  elincfzoext  13748  elfzonelfzo  13794  uzindi  14014  ssnn0fi  14017  sqlecan  14241  swrdnd2  14689  swrdwrdsymb  14696  wrd2ind  14756  repswccat  14819  cshwlen  14832  cshwidxmod  14836  2cshwcshw  14858  wrdl3s3  14995  lcmfunsnlem1  16690  coprmprod  16714  unbenlem  16963  infpnlem1  16965  prmgaplem7  17112  iscatd  17724  dirtr  18653  telgsums  20058  zrtermorngc  20742  zrtermoringc  20774  prmidlc  21473  psgndiflemA  21751  isphld  21804  gsummoncoe1  22468  gsummatr01lem3  22814  cpmatmcllem  22875  mp2pm2mplem4  22966  chfacfisf  23011  chfacfisfcpmat  23012  cayleyhamilton1  23049  tgcl  23126  neindisj2  23280  2ndcdisj  23613  fgcl  24035  rnelfm  24110  alexsubALTlem3  24206  2sqreultlem  27611  2sqreunnltlem  27614  elnnzs  28594  usgrexmpledg  29612  cusgrsize  29804  uspgr2wlkeqi  29997  usgr2wlkneq  30105  usgr2pthlem  30112  crctcshwlkn0  30170  wwlksnextinj  30248  wwlksnextproplem2  30259  wwlksnextproplem3  30260  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwwlkf1  30400  clwwlknwwlksnb  30406  clwwlkext2edg  30407  clwwlknonex2lem2  30459  frgr3vlem1  30624  3vfriswmgrlem  30628  vdgn1frgrv2  30647  frgrwopreglem5  30672  frgrwopreglem5ALT  30673  mdexchi  32687  atomli  32734  mdsymlem5  32759  sumdmdlem  32770  dfimafnf  32981  bnj517  35273  bnj1118  35372  mclsind  36062  dfon2lem6  36278  btwnconn1lem11  36589  finminlem  36849  isbasisrelowllem1  38021  isbasisrelowllem2  38022  poimirlem27  38318  itg2addnc  38345  rngoueqz  38611  dmncan1  38747  disjlem19  39573  lshpdisj  39781  2at0mat0  40319  llncvrlpln2  40351  lplncvrlvol2  40409  pmaple  40555  lhpexle2lem  40803  cdlemk33N  41703  cdlemk34  41704  sn-sup3d  43286  eldioph2  43513  cantnfresb  44071  gneispacess2  44892  sge0iunmpt  47152  funressnfv  47800  dfaimafn  47922  otiunsndisjX  48036  elfz2z  48072  iccelpart  48202  icceuelpart  48205  fargshiftfva  48212  sprsymrelfo  48266  sbcpr  48290  bgoldbtbndlem4  48593  grimcnv  48673  grimco  48674  clnbgrgrim  48719  uspgrlimlem4  48776  grlicsym  48798  grlictr  48800  pgnbgreunbgrlem3  48903  pgnbgreunbgrlem6  48909  idomcanl  49132  snlindsntor  49271  ldepspr  49273  nn0sumshdiglemB  49420