Theorem impancom 452

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 413	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	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 206  df-an 397

This theorem is referenced by:  mo4  2568  eqrdav  2739  spc2ed  3539  rexraleqim  3578  disjiun  5066  disjord  5067  disjiund  5069  propeqop  5425  euotd  5431  pwssun  5486  iotan0  6422  funopsn  7017  isotr  7203  funfv1st2nd  7880  funelss  7881  el2mpocsbcl  7916  ressuppssdif  7992  oeordi  8403  domunsncan  8841  pssnn  8933  pssnnOLD  9018  findcard3  9035  ordtypelem7  9261  inf3lem5  9368  r1tr  9535  cardmin2  9758  ac10ct  9791  isf32lem12  10121  isfin1-3  10143  fin17  10151  fin1a2s  10171  axdc4lem  10212  axcclem  10214  ttukeylem2  10267  genpcd  10763  ltexprlem3  10795  prlem936  10804  supsrlem  10868  mul0or  11615  un0addcl  12266  un0mulcl  12267  btwnnz  12396  uznfz  13338  elfz0ubfz0  13359  elfzo0z  13427  fzofzim  13432  ssfzoulel  13479  ssfzo12bi  13480  subfzo0  13507  modmuladdim  13632  modaddmodup  13652  modfzo0difsn  13661  axdc4uzlem  13701  expaddz  13825  sq01  13938  hashnn0n0nn  14104  hashss  14122  hashgt12el  14135  fi1uzind  14209  brfi1indALT  14212  ccatalpha  14296  swrdswrdlem  14415  swrdswrd  14416  swrdccatin1  14436  pfxccatin12lem3  14443  repswswrd  14495  cshf1  14521  cshw1  14533  2cshwcshw  14536  sqrmo  14961  caubnd2  15067  summo  15427  nno  16089  divalglem8  16107  lcmdvds  16311  lcmfunsnlem1  16340  hashgcdeq  16488  modprm0  16504  pcqcl  16555  vdwnnlem3  16696  prmgaplem5  16754  prmgaplem7  16756  catpropd  17416  cicsym  17514  isinitoi  17712  istermoi  17713  iszeroi  17722  acsfiindd  18269  tsrlemax  18302  issubg4  18772  gsmsymgreqlem2  19037  oddvdsnn0  19150  oddvds  19153  gexdvds  19187  lt6abl  19494  pgpfac1lem3  19678  isphld  20857  coe1ae0  21385  mdetdiaglem  21745  slesolex  21829  pmatcoe1fsupp  21848  cpmatelimp  21859  cpmatelimp2  21861  cpmatmcllem  21865  pm2mpf1  21946  mp2pm2mplem4  21956  fvmptnn04ifa  21997  fvmptnn04ifd  22000  chfacfscmul0  22005  chfacfpmmul0  22009  neii1  22255  neii2  22257  uncmp  22552  isfild  23007  fbunfip  23018  fgss2  23023  fgcl  23027  isufil2  23057  cfinufil  23077  ufilen  23079  fsumcn  24031  lmmbr  24420  iscau4  24441  caussi  24459  cmslssbn  24534  ovoliunnul  24669  ovolicc2lem4  24682  itg1ge0a  24874  rolle  25152  ulmcaulem  25551  cxpge0  25836  fsumvma  26359  gausslemma2dlem1a  26511  2sqb  26578  2sq2  26579  pntrsumbnd2  26713  pntlem3  26755  axeuclid  27329  axcontlem2  27331  usgrislfuspgr  27552  nbuhgr2vtx1edgblem  27716  usgredgsscusgredg  27824  upgrwlkvtxedg  28009  uspgr2wlkeq  28010  cyclnspth  28164  uspgrn2crct  28169  crctcshwlkn0lem4  28174  wlkiswwlks2lem5  28234  wlknewwlksn  28248  umgrwwlks2on  28318  clwwlkccatlem  28349  clwlkclwwlklem2a4  28357  clwlkclwwlklem2a  28358  clwwisshclwwslemlem  28373  clwwlkel  28406  wwlksubclwwlk  28418  clwwlknon1  28457  clwwlknonex2lem2  28468  uhgr3cyclexlem  28541  vdgn1frgrv3  28657  2wspmdisj  28697  frgrregord013  28755  spansncvi  30010  lnconi  30391  cdj3lem1  30792  metider  31840  prsrcmpltd  33051  gonar  33353  goalr  33355  satffunlem2lem1  33362  funeldmb  33733  nofv  33856  sltres  33861  finminlem  34503  clsint2  34514  bj-finsumval0  35452  finxpsuclem  35564  pibt2  35584  wl-exeq  35689  phpreu  35757  poimirlem26  35799  poimir  35806  ismtyima  35957  elpaddn0  37810  tendospcanN  39033  nnproddivdvdsd  40006  dvdsexpnn0  40338  rexzrexnn0  40623  unxpwdom3  40917  fsovrfovd  41587  radcnvrat  41902  2reu8i  44573  zm1nn  44763  subsubelfzo0  44787  fzoopth  44788  2ffzoeq  44789  fargshiftf  44861  2pwp1prm  45010  lighneal  45032  isomuspgrlem1  45248  isassintop  45373  uzlidlring  45456  2zrngamgm  45466  ply1mulgsumlem1  45696  suppdm  45820  rrxsphere  46063  inlinecirc02plem  46101