Theorem impancom 451

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

Ref	Expression
impancom.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impancom	⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 412	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	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:  mo4  2559  eqrdav  2728  spc2ed  3567  rexraleqim  3613  disjiun  5095  disjord  5096  disjiund  5098  propeqop  5467  euotd  5473  pwssun  5530  iotan0  6501  funopsn  7120  isotr  7311  funeldmb  7334  resf1extb  7910  funfv1st2nd  8025  funelss  8026  el2mpocsbcl  8064  ressuppssdif  8164  oeordi  8551  domunsncan  9041  pssnn  9132  findcard3  9229  findcard3OLD  9230  ordtypelem7  9477  inf3lem5  9585  r1tr  9729  cardmin2  9952  ac10ct  9987  isf32lem12  10317  isfin1-3  10339  fin17  10347  fin1a2s  10367  axdc4lem  10408  axcclem  10410  ttukeylem2  10463  genpcd  10959  ltexprlem3  10991  prlem936  11000  supsrlem  11064  mul0or  11818  un0addcl  12475  un0mulcl  12476  btwnnz  12610  uznfz  13571  elfz0ubfz0  13593  elfzo0z  13662  fzofzim  13670  ssfzoulel  13721  ssfzo12bi  13722  fzoopth  13723  subfzo0  13750  modmuladdim  13879  modaddmodup  13899  modfzo0difsn  13908  axdc4uzlem  13948  expaddz  14071  sq01  14190  hashnn0n0nn  14356  hashss  14374  hashgt12el  14387  fi1uzind  14472  brfi1indALT  14475  ccatalpha  14558  swrdswrdlem  14669  swrdswrd  14670  swrdccatin1  14690  pfxccatin12lem3  14697  repswswrd  14749  cshf1  14775  cshw1  14787  2cshwcshw  14791  sqrmo  15217  caubnd2  15324  summo  15683  nno  16352  divalglem8  16370  lcmdvds  16578  lcmfunsnlem1  16607  hashgcdeq  16760  modprm0  16776  pcqcl  16827  vdwnnlem3  16968  prmgaplem5  17026  prmgaplem7  17028  catpropd  17670  cicsym  17766  isinitoi  17961  istermoi  17962  iszeroi  17971  acsfiindd  18512  tsrlemax  18545  issubg4  19077  gsmsymgreqlem2  19361  oddvdsnn0  19474  oddvds  19477  gexdvds  19514  lt6abl  19825  pgpfac1lem3  20009  01eq0ring  20439  isphld  21563  psdmul  22053  coe1ae0  22101  mdetdiaglem  22485  slesolex  22569  pmatcoe1fsupp  22588  cpmatelimp  22599  cpmatelimp2  22601  cpmatmcllem  22605  pm2mpf1  22686  mp2pm2mplem4  22696  fvmptnn04ifa  22737  fvmptnn04ifd  22740  chfacfscmul0  22745  chfacfpmmul0  22749  neii1  22993  neii2  22995  uncmp  23290  isfild  23745  fbunfip  23756  fgss2  23761  fgcl  23765  isufil2  23795  cfinufil  23815  ufilen  23817  fsumcn  24761  lmmbr  25158  iscau4  25179  caussi  25197  cmslssbn  25272  ovoliunnul  25408  ovolicc2lem4  25421  itg1ge0a  25612  rolle  25894  ulmcaulem  26303  cxpge0  26592  fsumvma  27124  gausslemma2dlem1a  27276  2sqb  27343  2sq2  27344  pntrsumbnd2  27478  pntlem3  27520  nofv  27569  sltres  27574  muls0ord  28088  axeuclid  28890  axcontlem2  28892  usgrislfuspgr  29114  nbuhgr2vtx1edgblem  29278  usgredgsscusgredg  29387  upgrwlkvtxedg  29573  uspgr2wlkeq  29574  cyclnspth  29731  uspgrn2crct  29738  crctcshwlkn0lem4  29743  wlkiswwlks2lem5  29803  wlknewwlksn  29817  umgrwwlks2on  29887  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwwisshclwwslemlem  29942  clwwlkel  29975  wwlksubclwwlk  29987  clwwlknon1  30026  clwwlknonex2lem2  30037  uhgr3cyclexlem  30110  vdgn1frgrv3  30226  2wspmdisj  30266  frgrregord013  30324  spansncvi  31581  lnconi  31962  cdj3lem1  32363  constrsqrtcl  33769  metider  33884  prsrcmpltd  35071  onvf1odlem4  35093  gonar  35382  goalr  35384  satffunlem2lem1  35391  finminlem  36306  clsint2  36317  bj-finsumval0  37273  finxpsuclem  37385  pibt2  37405  wl-exeq  37522  phpreu  37598  poimirlem26  37640  poimir  37647  ismtyima  37797  elpaddn0  39794  tendospcanN  41017  nnproddivdvdsd  41988  dvdsexpnn0  42322  sn-remul0ord  42396  rexzrexnn0  42792  unxpwdom3  43084  unielss  43207  onov0suclim  43263  fsovrfovd  43998  radcnvrat  44303  2reu8i  47114  zm1nn  47303  subsubelfzo0  47327  2ffzoeq  47328  fargshiftf  47441  2pwp1prm  47590  lighneal  47612  isuspgrimlem  47895  upgrimpths  47909  gpgedgvtx0  48052  gpgedgvtx1  48053  isassintop  48198  uzlidlring  48223  2zrngamgm  48233  ply1mulgsumlem1  48375  suppdm  48499  rrxsphere  48737  inlinecirc02plem  48775  pgindnf  49705