Theorem impancom 457

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 418	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	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:  mo4  2592  spc2ed  3556  rexraleqim  3601  prsrcmpltd  4433  disjiun  5091  disjord  5092  disjiund  5094  propeqop  5479  euotd  5486  pwssun  5543  iotan0  6527  funopsn  7149  funopsnOLD  7150  isotr  7342  funeldmb  7367  resf1extb  7944  funfv1st2nd  8055  funelss  8056  el2mpocsbcl  8094  ressuppssdif  8195  oeordi  8589  domunsncan  9089  pssnn  9177  findcard3  9267  ordtypelem7  9511  inf3lem5  9626  r1tr  9776  cardmin2  10073  ac10ct  10106  isf32lem12  10435  isfin1-3  10457  fin17  10465  fin1a2s  10485  axdc4lem  10526  axcclem  10528  ttukeylem2  10581  genpcd  11084  ltexprlem3  11116  prlem936  11125  supsrlem  11189  mul0or  11949  un0addcl  12632  un0mulcl  12633  btwnnz  12768  uznfz  13737  elfz0ubfz0  13759  elfzo0z  13829  fzofzim  13837  ssfzoulel  13888  ssfzo12bi  13889  fzoopth  13890  subfzo0  13921  modmuladdim  14050  modaddmodup  14070  modfzo0difsn  14079  axdc4uzlem  14119  expaddz  14242  sq01  14362  hashnn0n0nn  14528  hashss  14546  hashgt12el  14560  fi1uzind  14645  brfi1indALT  14648  ccatalpha  14733  swrdswrdlem  14846  swrdswrd  14847  swrdccatin1  14867  pfxccatin12lem3  14874  repswswrd  14928  cshf1  14954  cshw1  14966  2cshwcshw  14969  sqrmo  15411  caubnd2  15518  summo  15876  nno  16545  divalglem8  16563  lcmdvds  16776  lcmfunsnlem1  16805  hashgcdeq  16960  modprm0  16976  pcqcl  17027  vdwnnlem3  17168  prmgaplem5  17226  prmgaplem7  17228  catpropd  17876  cicsym  17972  isinitoi  18167  istermoi  18168  iszeroi  18177  acsfiindd  18720  tsrlemax  18753  0gisid  18841  issubg4  19349  gsmsymgreqlem2  19638  oddvdsnn0  19751  oddvds  19754  gexdvds  19791  lt6abl  20102  pgpfac1lem3  20286  01eq0ring  20774  unichnlidl  21509  isphld  21953  psdmul  22480  coe1ae0  22527  mdetdiaglem  22906  slesolex  22993  pmatcoe1fsupp  23012  cpmatelimp  23023  cpmatelimp2  23025  cpmatmcllem  23029  pm2mpf1  23110  mp2pm2mplem4  23120  fvmptnn04ifa  23161  fvmptnn04ifd  23164  chfacfscmul0  23169  chfacfpmmul0  23173  neii1  23417  neii2  23419  uncmp  23714  isfild  24170  fbunfip  24181  fgss2  24186  fgcl  24190  isufil2  24220  cfinufil  24240  ufilen  24242  fsumcn  25184  lmmbr  25572  iscau4  25593  caussi  25611  cmslssbn  25686  ovoliunnul  25821  ovolicc2lem4  25834  itg1ge0a  26025  rolle  26303  ulmcaulem  26714  cxpge0  27004  fsumvma  27533  gausslemma2dlem1a  27685  2sqb  27752  2sq2  27753  pntrsumbnd2  27887  pntlem3  27929  nofv  28007  ltsres  28012  muls0ord  28564  axeuclid  29534  axcontlem2  29536  usgrislfuspgr  29761  nbuhgr2vtx1edgblem  29925  usgredgsscusgredg  30033  upgrwlkvtxedg  30218  uspgr2wlkeq  30219  cyclnspth  30382  uspgrn2crct  30390  crctcshwlkn0lem4  30395  wlkiswwlks2lem5  30455  wlknewwlksn  30469  usgrwwlks2on  30540  umgrwwlks2on  30541  clwwlkccatlem  30573  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwwisshclwwslemlem  30597  clwwlkel  30630  wwlksubclwwlk  30642  clwwlknon1  30681  clwwlknonex2lem2  30692  uhgr3cyclexlem  30775  vdgn1frgrv3  30891  2wspmdisj  30931  frgrregord013  30989  spansncvi  32247  lnconi  32628  cdj3lem1  33029  constrsqrtcl  34404  metider  34519  onvf1odlem4  35868  gonar  36139  goalr  36141  satffunlem2lem1  36148  finminlem  37086  clsint2  37097  cgsex2gd  38038  bj-finsumval0  38186  finxpsuclem  38300  pibt2  38320  wl-exeq  38446  phpreu  38507  poimirlem26  38544  poimir  38551  ismtyima  38717  elpaddn0  40837  tendospcanN  42060  nnproddivdvdsd  43030  dvdsexpnn0  43366  sn-remul0ord  43439  rexzrexnn0  43790  unxpwdom3  44081  unielss  44204  onov0suclim  44260  fsovrfovd  44994  radcnvrat  45283  2reu8i  48152  zm1nn  48341  subsubelfzo0  48366  2ffzoeq  48367  nnmul2  48369  fargshiftf  48491  2pwp1prm  48643  lighneal  48665  isuspgrimlem  48962  upgrimpths  48976  clnbgr3stgrgrlim  49086  gpgedgvtx0  49128  gpgedgvtx1  49129  isassintop  49276  uzlidlring  49301  2zrngamgm  49311  ply1mulgsumlem1  49467  suppdm  49591  rrxsphere  49829  inlinecirc02plem  49867  pgindnf  50778