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  2563  eqrdav  2732  spc2ed  3552  rexraleqim  3598  disjiun  5083  disjord  5084  disjiund  5086  propeqop  5452  euotd  5458  pwssun  5513  iotan0  6479  funopsn  7090  isotr  7279  funeldmb  7302  resf1extb  7873  funfv1st2nd  7987  funelss  7988  el2mpocsbcl  8024  ressuppssdif  8124  oeordi  8511  domunsncan  9001  pssnn  9089  findcard3  9178  ordtypelem7  9421  inf3lem5  9533  r1tr  9680  cardmin2  9903  ac10ct  9936  isf32lem12  10266  isfin1-3  10288  fin17  10296  fin1a2s  10316  axdc4lem  10357  axcclem  10359  ttukeylem2  10412  genpcd  10908  ltexprlem3  10940  prlem936  10949  supsrlem  11013  mul0or  11768  un0addcl  12425  un0mulcl  12426  btwnnz  12559  uznfz  13517  elfz0ubfz0  13539  elfzo0z  13608  fzofzim  13616  ssfzoulel  13667  ssfzo12bi  13668  fzoopth  13669  subfzo0  13699  modmuladdim  13828  modaddmodup  13848  modfzo0difsn  13857  axdc4uzlem  13897  expaddz  14020  sq01  14139  hashnn0n0nn  14305  hashss  14323  hashgt12el  14336  fi1uzind  14421  brfi1indALT  14424  ccatalpha  14508  swrdswrdlem  14618  swrdswrd  14619  swrdccatin1  14639  pfxccatin12lem3  14646  repswswrd  14698  cshf1  14724  cshw1  14736  2cshwcshw  14739  sqrmo  15165  caubnd2  15272  summo  15631  nno  16300  divalglem8  16318  lcmdvds  16526  lcmfunsnlem1  16555  hashgcdeq  16708  modprm0  16724  pcqcl  16775  vdwnnlem3  16916  prmgaplem5  16974  prmgaplem7  16976  catpropd  17623  cicsym  17719  isinitoi  17914  istermoi  17915  iszeroi  17924  acsfiindd  18467  tsrlemax  18500  issubg4  19066  gsmsymgreqlem2  19351  oddvdsnn0  19464  oddvds  19467  gexdvds  19504  lt6abl  19815  pgpfac1lem3  19999  01eq0ring  20454  isphld  21600  psdmul  22100  coe1ae0  22148  mdetdiaglem  22533  slesolex  22617  pmatcoe1fsupp  22636  cpmatelimp  22647  cpmatelimp2  22649  cpmatmcllem  22653  pm2mpf1  22734  mp2pm2mplem4  22744  fvmptnn04ifa  22785  fvmptnn04ifd  22788  chfacfscmul0  22793  chfacfpmmul0  22797  neii1  23041  neii2  23043  uncmp  23338  isfild  23793  fbunfip  23804  fgss2  23809  fgcl  23813  isufil2  23843  cfinufil  23863  ufilen  23865  fsumcn  24808  lmmbr  25205  iscau4  25226  caussi  25244  cmslssbn  25319  ovoliunnul  25455  ovolicc2lem4  25468  itg1ge0a  25659  rolle  25941  ulmcaulem  26350  cxpge0  26639  fsumvma  27171  gausslemma2dlem1a  27323  2sqb  27390  2sq2  27391  pntrsumbnd2  27525  pntlem3  27567  nofv  27616  sltres  27621  muls0ord  28144  axeuclid  28962  axcontlem2  28964  usgrislfuspgr  29186  nbuhgr2vtx1edgblem  29350  usgredgsscusgredg  29459  upgrwlkvtxedg  29644  uspgr2wlkeq  29645  cyclnspth  29800  uspgrn2crct  29807  crctcshwlkn0lem4  29812  wlkiswwlks2lem5  29872  wlknewwlksn  29886  usgrwwlks2on  29957  umgrwwlks2on  29958  clwwlkccatlem  29990  clwlkclwwlklem2a4  29998  clwlkclwwlklem2a  29999  clwwisshclwwslemlem  30014  clwwlkel  30047  wwlksubclwwlk  30059  clwwlknon1  30098  clwwlknonex2lem2  30109  uhgr3cyclexlem  30182  vdgn1frgrv3  30298  2wspmdisj  30338  frgrregord013  30396  spansncvi  31653  lnconi  32034  cdj3lem1  32435  constrsqrtcl  33864  metider  33979  prsrcmpltd  35165  onvf1odlem4  35222  gonar  35511  goalr  35513  satffunlem2lem1  35520  finminlem  36434  clsint2  36445  bj-finsumval0  37402  finxpsuclem  37514  pibt2  37534  wl-exeq  37651  phpreu  37717  poimirlem26  37759  poimir  37766  ismtyima  37916  elpaddn0  39972  tendospcanN  41195  nnproddivdvdsd  42166  dvdsexpnn0  42504  sn-remul0ord  42578  rexzrexnn0  42961  unxpwdom3  43252  unielss  43375  onov0suclim  43431  fsovrfovd  44166  radcnvrat  44471  2reu8i  47275  zm1nn  47464  subsubelfzo0  47488  2ffzoeq  47489  fargshiftf  47602  2pwp1prm  47751  lighneal  47773  isuspgrimlem  48057  upgrimpths  48071  clnbgr3stgrgrlim  48181  gpgedgvtx0  48223  gpgedgvtx1  48224  isassintop  48372  uzlidlring  48397  2zrngamgm  48407  ply1mulgsumlem1  48548  suppdm  48672  rrxsphere  48910  inlinecirc02plem  48948  pgindnf  49877