Theorem imp31 423

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp41  431  imp5d  445  impl  461  anassrs  473  an31s  667  3imp  1128  reusv3  5374  otiunsndisj  5500  pwssun  5550  ordelord  6410  tz7.7  6414  dfimafn  6978  funimass4  6980  funimass3  7084  isomin  7376  isopolem  7384  onint  7838  limsssuc  7895  tfindsg  7906  findsg  7943  suppfnss  8244  smores2  8400  tfrlem9  8431  tz7.49  8493  oecl  8583  oaordi  8592  oaass  8607  omordi  8612  odi  8625  oen0  8633  nnaordi  8665  nnmordi  8678  domunfican  9351  dfac5  10246  cofsmo  10386  cfcoflem  10389  zorn2lem7  10619  tskwun  10908  mulcanpi  11024  ltexprlem7  11166  sup3  12314  elnnz  12743  nzadd  12784  irradd  13141  irrmul  13142  uzsubsubfz  13720  fzo1fzo0n0  13890  elincfzoext  13898  elfzonelfzo  13944  uzindi  14165  ssnn0fi  14168  sqlecan  14393  swrdnd2  14847  swrdwrdsymb  14854  wrd2ind  14914  repswccat  14979  cshwlen  14992  cshwidxmod  14996  2cshwcshw  15018  wrdl3s3  15158  lcmfunsnlem1  16856  coprmprod  16880  unbenlem  17130  infpnlem1  17132  prmgaplem7  17279  iscatd  17897  dirtr  18826  telgsums  20258  zrtermorngc  20946  zrtermoringc  20978  prmidlc  21680  psgndiflemA  21962  isphld  22015  gsummoncoe1  22681  gsummatr01lem3  23027  cpmatmcllem  23091  mp2pm2mplem4  23182  chfacfisf  23227  chfacfisfcpmat  23228  cayleyhamilton1  23265  tgcl  23342  neindisj2  23496  2ndcdisj  23830  fgcl  24252  rnelfm  24327  alexsubALTlem3  24423  2sqreultlem  27831  2sqreunnltlem  27834  elnnzs  28844  usgrexmpledg  29900  cusgrsize  30092  uspgr2wlkeqi  30285  usgr2wlkneq  30399  usgr2pthlem  30406  crctcshwlkn0  30467  wwlksnextinj  30545  wwlksnextproplem2  30556  wwlksnextproplem3  30557  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwwlkf1  30697  clwwlknwwlksnb  30703  clwwlkext2edg  30704  clwwlknonex2lem2  30756  frgr3vlem1  30931  3vfriswmgrlem  30935  vdgn1frgrv2  30954  frgrwopreglem5  30979  frgrwopreglem5ALT  30980  mdexchi  32994  atomli  33041  mdsymlem5  33066  sumdmdlem  33077  dfimafnf  33328  bnj517  35626  bnj1118  35725  mclsind  36543  dfon2lem6  36765  btwnconn1lem11  37077  finminlem  37321  isbasisrelowllem1  38546  isbasisrelowllem2  38547  poimirlem27  38833  itg2addnc  38860  rngoueqz  39140  dmncan1  39276  disjlem19  40102  lshpdisj  40310  2at0mat0  40848  llncvrlpln2  40880  lplncvrlvol2  40938  pmaple  41084  lhpexle2lem  41332  cdlemk33N  42232  cdlemk34  42233  sn-sup3d  43822  eldioph2  44039  cantnfresb  44587  gneispacess2  45407  sge0iunmpt  47701  funressnfv  48386  dfaimafn  48508  otiunsndisjX  48622  elfz2z  48658  iccelpart  48788  icceuelpart  48791  fargshiftfva  48798  sprsymrelfo  48852  sbcpr  48876  bgoldbtbndlem4  49179  grimcnv  49259  grimco  49260  clnbgrgrim  49305  uspgrlimlem4  49362  grlicsym  49384  grlictr  49386  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  idomcanl  49775  snlindsntor  49914  ldepspr  49916  nn0sumshdiglemB  50063