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  654  3imp  1110  reusv3  5410  otiunsndisj  5529  pwssun  5579  friOLD  5646  ordelord  6407  tz7.7  6411  dfimafn  6970  funimass4  6972  funimass3  7073  isomin  7356  isopolem  7364  onint  7809  limsssuc  7870  tfindsg  7881  findsg  7919  suppfnss  8212  smores2  8392  tfrlem9  8423  tz7.49  8483  oecl  8573  oaordi  8582  oaass  8597  omordi  8602  odi  8615  oen0  8622  nnaordi  8654  nnmordi  8667  php3OLD  9258  domunfican  9358  dfac5  10166  cofsmo  10306  cfcoflem  10309  zorn2lem7  10539  tskwun  10821  mulcanpi  10937  ltexprlem7  11079  sup3  12222  elnnz  12620  nzadd  12662  irradd  13012  irrmul  13013  uzsubsubfz  13582  fzo1fzo0n0  13750  elincfzoext  13758  elfzonelfzo  13804  uzindi  14019  ssnn0fi  14022  sqlecan  14244  swrdnd2  14689  swrdwrdsymb  14696  wrd2ind  14757  repswccat  14820  cshwlen  14833  cshwidxmod  14837  2cshwcshw  14860  wrdl3s3  14997  lcmfunsnlem1  16670  coprmprod  16694  unbenlem  16941  infpnlem1  16943  prmgaplem7  17090  iscatd  17717  dirtr  18659  telgsums  20025  zrtermorngc  20659  zrtermoringc  20691  psgndiflemA  21636  isphld  21689  gsummoncoe1  22327  gsummatr01lem3  22678  cpmatmcllem  22739  mp2pm2mplem4  22830  chfacfisf  22875  chfacfisfcpmat  22876  cayleyhamilton1  22913  tgcl  22991  neindisj2  23146  2ndcdisj  23479  fgcl  23901  rnelfm  23976  alexsubALTlem3  24072  2sqreultlem  27505  2sqreunnltlem  27508  elnnzs  28401  usgrexmpledg  29293  cusgrsize  29486  uspgr2wlkeqi  29680  usgr2wlkneq  29788  usgr2pthlem  29795  crctcshwlkn0  29850  wwlksnextinj  29928  wwlksnextproplem2  29939  wwlksnextproplem3  29940  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwwlkf1  30077  clwwlknwwlksnb  30083  clwwlkext2edg  30084  clwwlknonex2lem2  30136  frgr3vlem1  30301  3vfriswmgrlem  30305  vdgn1frgrv2  30324  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  mdexchi  32363  atomli  32410  mdsymlem5  32435  sumdmdlem  32446  dfimafnf  32652  prmidlc  33455  bnj517  34877  bnj1118  34976  mclsind  35554  dfon2lem6  35769  btwnconn1lem11  36078  finminlem  36300  isbasisrelowllem1  37337  isbasisrelowllem2  37338  poimirlem27  37633  itg2addnc  37660  rngoueqz  37926  dmncan1  38062  disjlem19  38782  lshpdisj  38968  2at0mat0  39507  llncvrlpln2  39539  lplncvrlvol2  39597  lhpexle2lem  39991  cdlemk33N  40891  cdlemk34  40892  sn-sup3d  42478  eldioph2  42749  cantnfresb  43313  gneispacess2  44135  sge0iunmpt  46373  funressnfv  46992  dfaimafn  47114  otiunsndisjX  47228  elfz2z  47264  iccelpart  47357  icceuelpart  47360  fargshiftfva  47367  sprsymrelfo  47421  sbcpr  47445  bgoldbtbndlem4  47732  grimcnv  47816  grimco  47817  clnbgrgrim  47839  uspgrlimlem4  47893  grlicsym  47908  grlictr  47910  snlindsntor  48316  ldepspr  48318  nn0sumshdiglemB  48469