Theorem imp31 421

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  imp41  429  imp5d  443  impl  459  anassrs  471  an31s  653  3imp  1108  reusv3  5278  otiunsndisj  5383  pwssun  5430  fri  5490  predpo  6149  ordelord  6196  tz7.7  6200  dfimafn  6721  funimass4  6723  funimass3  6820  isomin  7090  isopolem  7098  onint  7515  limsssuc  7570  tfindsg  7580  findsg  7615  suppfnss  7869  smores2  8007  tfrlem9  8037  tz7.49  8097  oecl  8178  oaordi  8188  oaass  8203  omordi  8208  odi  8221  oen0  8228  nnaordi  8260  nnmordi  8273  php3  8738  domunfican  8837  dfac5  9601  cofsmo  9742  cfcoflem  9745  zorn2lem7  9975  tskwun  10257  mulcanpi  10373  ltexprlem7  10515  sup3  11647  elnnz  12043  nzadd  12082  irradd  12426  irrmul  12427  uzsubsubfz  12991  fzo1fzo0n0  13150  elincfzoext  13157  elfzonelfzo  13201  uzindi  13412  ssnn0fi  13415  sqlecan  13634  swrdnd2  14077  swrdwrdsymb  14084  wrd2ind  14145  repswccat  14208  cshwlen  14221  cshwidxmod  14225  2cshwcshw  14247  wrdl3s3  14386  lcmfunsnlem1  16047  coprmprod  16071  unbenlem  16313  infpnlem1  16315  prmgaplem7  16462  iscatd  17016  dirtr  17926  telgsums  19195  psgndiflemA  20380  isphld  20433  psrbaglefiOLD  20709  gsummoncoe1  21042  gsummatr01lem3  21371  cpmatmcllem  21432  mp2pm2mplem4  21523  chfacfisf  21568  chfacfisfcpmat  21569  cayleyhamilton1  21606  tgcl  21683  neindisj2  21837  2ndcdisj  22170  fgcl  22592  rnelfm  22667  alexsubALTlem3  22763  2sqreultlem  26144  2sqreunnltlem  26147  usgrexmpledg  27165  cusgrsize  27357  uspgr2wlkeqi  27550  usgr2wlkneq  27658  usgr2pthlem  27665  crctcshwlkn0  27720  wwlksnextinj  27798  wwlksnextproplem2  27809  wwlksnextproplem3  27810  clwlkclwwlklem2a  27896  clwlkclwwlklem2  27898  clwwlkf1  27947  clwwlknwwlksnb  27953  clwwlkext2edg  27954  clwwlknonex2lem2  28006  frgr3vlem1  28171  3vfriswmgrlem  28175  vdgn1frgrv2  28194  frgrwopreglem5  28219  frgrwopreglem5ALT  28220  mdexchi  30231  atomli  30278  mdsymlem5  30303  sumdmdlem  30314  dfimafnf  30507  prmidlc  31158  bnj517  32398  bnj1118  32497  mclsind  33061  dfon2lem6  33293  btwnconn1lem11  33983  finminlem  34091  isbasisrelowllem1  35087  isbasisrelowllem2  35088  poimirlem27  35399  itg2addnc  35426  rngoueqz  35693  dmncan1  35829  lshpdisj  36598  2at0mat0  37136  llncvrlpln2  37168  lplncvrlvol2  37226  lhpexle2lem  37620  cdlemk33N  38520  cdlemk34  38521  eldioph2  40121  gneispacess2  41267  sge0iunmpt  43468  funressnfv  44046  dfaimafn  44148  otiunsndisjX  44262  elfz2z  44299  iccelpart  44377  icceuelpart  44380  fargshiftfva  44387  sprsymrelfo  44441  sbcpr  44465  bgoldbtbndlem4  44752  isomuspgrlem1  44771  isomuspgrlem2b  44773  isomuspgrlem2d  44775  zrtermorngc  45051  zrtermoringc  45120  snlindsntor  45304  ldepspr  45306  nn0sumshdiglemB  45458