Theorem imp31 418

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp41  426  imp5d  440  impl  456  anassrs  468  an31s  650  3imp  1104  reusv3  5202  otiunsndisj  5306  pwssun  5349  fri  5410  predpo  6046  ordelord  6093  tz7.7  6097  dfimafn  6601  funimass4  6603  funimass3  6694  isomin  6958  isopolem  6966  onint  7371  limsssuc  7426  tfindsg  7436  findsg  7470  suppfnss  7711  smores2  7848  tfrlem9  7878  tz7.49  7937  oecl  8018  oaordi  8027  oaass  8042  omordi  8047  odi  8060  oen0  8067  nnaordi  8099  nnmordi  8112  php3  8555  domunfican  8642  dfac5  9405  cofsmo  9542  cfcoflem  9545  zorn2lem7  9775  tskwun  10057  mulcanpi  10173  ltexprlem7  10315  sup3  11451  elnnz  11844  nzadd  11884  irradd  12227  irrmul  12228  uzsubsubfz  12784  fzo1fzo0n0  12943  elincfzoext  12950  elfzonelfzo  12994  uzindi  13205  ssnn0fi  13208  sqlecan  13426  swrdnd2  13858  swrdwrdsymb  13865  wrd2ind  13926  repswccat  13989  cshwlen  14002  cshwidxmod  14006  2cshwcshw  14028  wrdl3s3  14165  lcmfunsnlem1  15815  coprmprod  15839  unbenlem  16078  infpnlem1  16080  prmgaplem7  16227  iscatd  16778  dirtr  17680  telgsums  18835  psrbaglefi  19845  gsummoncoe1  20160  psgndiflemA  20432  isphld  20485  gsummatr01lem3  20955  cpmatmcllem  21015  mp2pm2mplem4  21106  chfacfisf  21151  chfacfisfcpmat  21152  cayleyhamilton1  21189  tgcl  21266  neindisj2  21420  2ndcdisj  21753  fgcl  22175  rnelfm  22250  alexsubALTlem3  22346  2sqreultlem  25710  2sqreunnltlem  25713  usgrexmpledg  26732  cusgrsize  26924  uspgr2wlkeqi  27117  usgr2wlkneq  27229  usgr2pthlem  27236  crctcshwlkn0  27291  wwlksnextinj  27369  wwlksnextproplem2  27381  wwlksnextproplem3  27382  clwlkclwwlklem2a  27468  clwlkclwwlklem2  27470  clwwlkf1  27520  clwwlknwwlksnb  27526  clwwlkext2edg  27527  wwlksext2clwwlk  27528  clwwlknonex2lem2  27579  frgr3vlem1  27749  3vfriswmgrlem  27753  vdgn1frgrv2  27772  frgrwopreglem5  27797  frgrwopreglem5ALT  27798  mdexchi  29808  atomli  29855  mdsymlem5  29880  sumdmdlem  29891  dfimafnf  30076  bnj517  31778  bnj1118  31875  mclsind  32431  dfon2lem6  32647  btwnconn1lem11  33173  finminlem  33281  bj-snmoore  34030  isbasisrelowllem1  34192  isbasisrelowllem2  34193  poimirlem27  34475  itg2addnc  34502  rngoueqz  34775  dmncan1  34911  lshpdisj  35679  2at0mat0  36217  llncvrlpln2  36249  lplncvrlvol2  36307  lhpexle2lem  36701  cdlemk33N  37601  cdlemk34  37602  eldioph2  38869  gneispacess2  40006  sge0iunmpt  42268  funressnfv  42820  dfaimafn  42906  otiunsndisjX  43020  elfz2z  43057  iccelpart  43101  icceuelpart  43104  fargshiftfva  43111  sprsymrelfo  43167  sbcpr  43191  bgoldbtbndlem4  43481  isomuspgrlem1  43500  isomuspgrlem2b  43502  isomuspgrlem2d  43504  zrtermorngc  43776  zrtermoringc  43845  snlindsntor  44032  ldepspr  44034  nn0sumshdiglemB  44187