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  5355  otiunsndisj  5475  pwssun  5523  ordelord  6342  tz7.7  6346  dfimafn  6905  funimass4  6907  funimass3  7008  isomin  7294  isopolem  7302  onint  7746  limsssuc  7806  tfindsg  7817  findsg  7853  suppfnss  8145  smores2  8300  tfrlem9  8330  tz7.49  8390  oecl  8478  oaordi  8487  oaass  8502  omordi  8507  odi  8520  oen0  8527  nnaordi  8559  nnmordi  8572  domunfican  9248  dfac5  10058  cofsmo  10198  cfcoflem  10201  zorn2lem7  10431  tskwun  10713  mulcanpi  10829  ltexprlem7  10971  sup3  12116  elnnz  12515  nzadd  12557  irradd  12908  irrmul  12909  uzsubsubfz  13483  fzo1fzo0n0  13652  elincfzoext  13660  elfzonelfzo  13706  uzindi  13923  ssnn0fi  13926  sqlecan  14150  swrdnd2  14596  swrdwrdsymb  14603  wrd2ind  14664  repswccat  14727  cshwlen  14740  cshwidxmod  14744  2cshwcshw  14767  wrdl3s3  14904  lcmfunsnlem1  16583  coprmprod  16607  unbenlem  16855  infpnlem1  16857  prmgaplem7  17004  iscatd  17614  dirtr  18543  telgsums  19907  zrtermorngc  20563  zrtermoringc  20595  psgndiflemA  21543  isphld  21596  gsummoncoe1  22228  gsummatr01lem3  22577  cpmatmcllem  22638  mp2pm2mplem4  22729  chfacfisf  22774  chfacfisfcpmat  22775  cayleyhamilton1  22812  tgcl  22889  neindisj2  23043  2ndcdisj  23376  fgcl  23798  rnelfm  23873  alexsubALTlem3  23969  2sqreultlem  27391  2sqreunnltlem  27394  elnnzs  28329  usgrexmpledg  29242  cusgrsize  29435  uspgr2wlkeqi  29628  usgr2wlkneq  29736  usgr2pthlem  29743  crctcshwlkn0  29801  wwlksnextinj  29879  wwlksnextproplem2  29890  wwlksnextproplem3  29891  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  clwwlkf1  30028  clwwlknwwlksnb  30034  clwwlkext2edg  30035  clwwlknonex2lem2  30087  frgr3vlem1  30252  3vfriswmgrlem  30256  vdgn1frgrv2  30275  frgrwopreglem5  30300  frgrwopreglem5ALT  30301  mdexchi  32314  atomli  32361  mdsymlem5  32386  sumdmdlem  32397  dfimafnf  32610  prmidlc  33412  bnj517  34868  bnj1118  34967  mclsind  35550  dfon2lem6  35769  btwnconn1lem11  36078  finminlem  36299  isbasisrelowllem1  37336  isbasisrelowllem2  37337  poimirlem27  37634  itg2addnc  37661  rngoueqz  37927  dmncan1  38063  disjlem19  38786  lshpdisj  38973  2at0mat0  39512  llncvrlpln2  39544  lplncvrlvol2  39602  lhpexle2lem  39996  cdlemk33N  40896  cdlemk34  40897  sn-sup3d  42473  eldioph2  42743  cantnfresb  43306  gneispacess2  44128  sge0iunmpt  46409  funressnfv  47037  dfaimafn  47159  otiunsndisjX  47273  elfz2z  47309  iccelpart  47427  icceuelpart  47430  fargshiftfva  47437  sprsymrelfo  47491  sbcpr  47515  bgoldbtbndlem4  47802  grimcnv  47881  grimco  47882  clnbgrgrim  47927  uspgrlimlem4  47983  grlicsym  47998  grlictr  48000  pgnbgreunbgrlem3  48101  pgnbgreunbgrlem6  48107  snlindsntor  48453  ldepspr  48455  nn0sumshdiglemB  48602