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  5352  otiunsndisj  5476  pwssun  5524  ordelord  6347  tz7.7  6351  dfimafn  6904  funimass4  6906  funimass3  7008  isomin  7293  isopolem  7301  onint  7745  limsssuc  7802  tfindsg  7813  findsg  7849  suppfnss  8141  smores2  8296  tfrlem9  8326  tz7.49  8386  oecl  8474  oaordi  8483  oaass  8498  omordi  8503  odi  8516  oen0  8524  nnaordi  8556  nnmordi  8569  domunfican  9234  dfac5  10051  cofsmo  10191  cfcoflem  10194  zorn2lem7  10424  tskwun  10707  mulcanpi  10823  ltexprlem7  10965  sup3  12111  elnnz  12510  nzadd  12551  irradd  12898  irrmul  12899  uzsubsubfz  13474  fzo1fzo0n0  13643  elincfzoext  13651  elfzonelfzo  13697  uzindi  13917  ssnn0fi  13920  sqlecan  14144  swrdnd2  14591  swrdwrdsymb  14598  wrd2ind  14658  repswccat  14721  cshwlen  14734  cshwidxmod  14738  2cshwcshw  14760  wrdl3s3  14897  lcmfunsnlem1  16576  coprmprod  16600  unbenlem  16848  infpnlem1  16850  prmgaplem7  16997  iscatd  17608  dirtr  18537  telgsums  19934  zrtermorngc  20588  zrtermoringc  20620  psgndiflemA  21568  isphld  21621  gsummoncoe1  22264  gsummatr01lem3  22613  cpmatmcllem  22674  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  cayleyhamilton1  22848  tgcl  22925  neindisj2  23079  2ndcdisj  23412  fgcl  23834  rnelfm  23909  alexsubALTlem3  24005  2sqreultlem  27426  2sqreunnltlem  27429  elnnzs  28409  usgrexmpledg  29347  cusgrsize  29540  uspgr2wlkeqi  29733  usgr2wlkneq  29841  usgr2pthlem  29848  crctcshwlkn0  29906  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwlkf1  30136  clwwlknwwlksnb  30142  clwwlkext2edg  30143  clwwlknonex2lem2  30195  frgr3vlem1  30360  3vfriswmgrlem  30364  vdgn1frgrv2  30383  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  mdexchi  32423  atomli  32470  mdsymlem5  32495  sumdmdlem  32506  dfimafnf  32726  prmidlc  33541  bnj517  35061  bnj1118  35160  mclsind  35786  dfon2lem6  36002  btwnconn1lem11  36313  finminlem  36534  isbasisrelowllem1  37610  isbasisrelowllem2  37611  poimirlem27  37898  itg2addnc  37925  rngoueqz  38191  dmncan1  38327  disjlem19  39155  lshpdisj  39363  2at0mat0  39901  llncvrlpln2  39933  lplncvrlvol2  39991  pmaple  40137  lhpexle2lem  40385  cdlemk33N  41285  cdlemk34  41286  sn-sup3d  42862  eldioph2  43119  cantnfresb  43681  gneispacess2  44502  sge0iunmpt  46776  funressnfv  47403  dfaimafn  47525  otiunsndisjX  47639  elfz2z  47675  iccelpart  47793  icceuelpart  47796  fargshiftfva  47803  sprsymrelfo  47857  sbcpr  47881  bgoldbtbndlem4  48168  grimcnv  48248  grimco  48249  clnbgrgrim  48294  uspgrlimlem4  48351  grlicsym  48373  grlictr  48375  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  snlindsntor  48831  ldepspr  48833  nn0sumshdiglemB  48980