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 206  df-an 396

This theorem is referenced by:  imp41  425  imp5d  439  impl  455  anassrs  467  an31s  650  3imp  1109  reusv3  5323  otiunsndisj  5428  pwssun  5476  friOLD  5541  ordelord  6273  tz7.7  6277  dfimafn  6814  funimass4  6816  funimass3  6913  isomin  7188  isopolem  7196  onint  7617  limsssuc  7672  tfindsg  7682  findsg  7720  suppfnss  7976  smores2  8156  tfrlem9  8187  tz7.49  8246  oecl  8329  oaordi  8339  oaass  8354  omordi  8359  odi  8372  oen0  8379  nnaordi  8411  nnmordi  8424  php3  8899  domunfican  9017  dfac5  9815  cofsmo  9956  cfcoflem  9959  zorn2lem7  10189  tskwun  10471  mulcanpi  10587  ltexprlem7  10729  sup3  11862  elnnz  12259  nzadd  12298  irradd  12642  irrmul  12643  uzsubsubfz  13207  fzo1fzo0n0  13366  elincfzoext  13373  elfzonelfzo  13417  uzindi  13630  ssnn0fi  13633  sqlecan  13853  swrdnd2  14296  swrdwrdsymb  14303  wrd2ind  14364  repswccat  14427  cshwlen  14440  cshwidxmod  14444  2cshwcshw  14466  wrdl3s3  14605  lcmfunsnlem1  16270  coprmprod  16294  unbenlem  16537  infpnlem1  16539  prmgaplem7  16686  iscatd  17299  dirtr  18235  telgsums  19509  psgndiflemA  20718  isphld  20771  psrbaglefiOLD  21046  gsummoncoe1  21385  gsummatr01lem3  21714  cpmatmcllem  21775  mp2pm2mplem4  21866  chfacfisf  21911  chfacfisfcpmat  21912  cayleyhamilton1  21949  tgcl  22027  neindisj2  22182  2ndcdisj  22515  fgcl  22937  rnelfm  23012  alexsubALTlem3  23108  2sqreultlem  26500  2sqreunnltlem  26503  usgrexmpledg  27532  cusgrsize  27724  uspgr2wlkeqi  27917  usgr2wlkneq  28025  usgr2pthlem  28032  crctcshwlkn0  28087  wwlksnextinj  28165  wwlksnextproplem2  28176  wwlksnextproplem3  28177  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwwlkf1  28314  clwwlknwwlksnb  28320  clwwlkext2edg  28321  clwwlknonex2lem2  28373  frgr3vlem1  28538  3vfriswmgrlem  28542  vdgn1frgrv2  28561  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  mdexchi  30598  atomli  30645  mdsymlem5  30670  sumdmdlem  30681  dfimafnf  30872  prmidlc  31526  bnj517  32765  bnj1118  32864  mclsind  33432  dfon2lem6  33670  btwnconn1lem11  34326  finminlem  34434  isbasisrelowllem1  35453  isbasisrelowllem2  35454  poimirlem27  35731  itg2addnc  35758  rngoueqz  36025  dmncan1  36161  lshpdisj  36928  2at0mat0  37466  llncvrlpln2  37498  lplncvrlvol2  37556  lhpexle2lem  37950  cdlemk33N  38850  cdlemk34  38851  eldioph2  40500  gneispacess2  41645  sge0iunmpt  43846  funressnfv  44424  dfaimafn  44544  otiunsndisjX  44658  elfz2z  44695  iccelpart  44773  icceuelpart  44776  fargshiftfva  44783  sprsymrelfo  44837  sbcpr  44861  bgoldbtbndlem4  45148  isomuspgrlem1  45167  isomuspgrlem2b  45169  isomuspgrlem2d  45171  zrtermorngc  45447  zrtermoringc  45516  snlindsntor  45700  ldepspr  45702  nn0sumshdiglemB  45854