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  2560  eqrdav  2729  spc2ed  3570  rexraleqim  3616  disjiun  5098  disjord  5099  disjiund  5101  propeqop  5470  euotd  5476  pwssun  5533  iotan0  6504  funopsn  7123  isotr  7314  funeldmb  7337  resf1extb  7913  funfv1st2nd  8028  funelss  8029  el2mpocsbcl  8067  ressuppssdif  8167  oeordi  8554  domunsncan  9046  pssnn  9138  findcard3  9236  findcard3OLD  9237  ordtypelem7  9484  inf3lem5  9592  r1tr  9736  cardmin2  9959  ac10ct  9994  isf32lem12  10324  isfin1-3  10346  fin17  10354  fin1a2s  10374  axdc4lem  10415  axcclem  10417  ttukeylem2  10470  genpcd  10966  ltexprlem3  10998  prlem936  11007  supsrlem  11071  mul0or  11825  un0addcl  12482  un0mulcl  12483  btwnnz  12617  uznfz  13578  elfz0ubfz0  13600  elfzo0z  13669  fzofzim  13677  ssfzoulel  13728  ssfzo12bi  13729  fzoopth  13730  subfzo0  13757  modmuladdim  13886  modaddmodup  13906  modfzo0difsn  13915  axdc4uzlem  13955  expaddz  14078  sq01  14197  hashnn0n0nn  14363  hashss  14381  hashgt12el  14394  fi1uzind  14479  brfi1indALT  14482  ccatalpha  14565  swrdswrdlem  14676  swrdswrd  14677  swrdccatin1  14697  pfxccatin12lem3  14704  repswswrd  14756  cshf1  14782  cshw1  14794  2cshwcshw  14798  sqrmo  15224  caubnd2  15331  summo  15690  nno  16359  divalglem8  16377  lcmdvds  16585  lcmfunsnlem1  16614  hashgcdeq  16767  modprm0  16783  pcqcl  16834  vdwnnlem3  16975  prmgaplem5  17033  prmgaplem7  17035  catpropd  17677  cicsym  17773  isinitoi  17968  istermoi  17969  iszeroi  17978  acsfiindd  18519  tsrlemax  18552  issubg4  19084  gsmsymgreqlem2  19368  oddvdsnn0  19481  oddvds  19484  gexdvds  19521  lt6abl  19832  pgpfac1lem3  20016  01eq0ring  20446  isphld  21570  psdmul  22060  coe1ae0  22108  mdetdiaglem  22492  slesolex  22576  pmatcoe1fsupp  22595  cpmatelimp  22606  cpmatelimp2  22608  cpmatmcllem  22612  pm2mpf1  22693  mp2pm2mplem4  22703  fvmptnn04ifa  22744  fvmptnn04ifd  22747  chfacfscmul0  22752  chfacfpmmul0  22756  neii1  23000  neii2  23002  uncmp  23297  isfild  23752  fbunfip  23763  fgss2  23768  fgcl  23772  isufil2  23802  cfinufil  23822  ufilen  23824  fsumcn  24768  lmmbr  25165  iscau4  25186  caussi  25204  cmslssbn  25279  ovoliunnul  25415  ovolicc2lem4  25428  itg1ge0a  25619  rolle  25901  ulmcaulem  26310  cxpge0  26599  fsumvma  27131  gausslemma2dlem1a  27283  2sqb  27350  2sq2  27351  pntrsumbnd2  27485  pntlem3  27527  nofv  27576  sltres  27581  muls0ord  28095  axeuclid  28897  axcontlem2  28899  usgrislfuspgr  29121  nbuhgr2vtx1edgblem  29285  usgredgsscusgredg  29394  upgrwlkvtxedg  29580  uspgr2wlkeq  29581  cyclnspth  29738  uspgrn2crct  29745  crctcshwlkn0lem4  29750  wlkiswwlks2lem5  29810  wlknewwlksn  29824  umgrwwlks2on  29894  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwwisshclwwslemlem  29949  clwwlkel  29982  wwlksubclwwlk  29994  clwwlknon1  30033  clwwlknonex2lem2  30044  uhgr3cyclexlem  30117  vdgn1frgrv3  30233  2wspmdisj  30273  frgrregord013  30331  spansncvi  31588  lnconi  31969  cdj3lem1  32370  constrsqrtcl  33776  metider  33891  prsrcmpltd  35078  onvf1odlem4  35100  gonar  35389  goalr  35391  satffunlem2lem1  35398  finminlem  36313  clsint2  36324  bj-finsumval0  37280  finxpsuclem  37392  pibt2  37412  wl-exeq  37529  phpreu  37605  poimirlem26  37647  poimir  37654  ismtyima  37804  elpaddn0  39801  tendospcanN  41024  nnproddivdvdsd  41995  dvdsexpnn0  42329  sn-remul0ord  42403  rexzrexnn0  42799  unxpwdom3  43091  unielss  43214  onov0suclim  43270  fsovrfovd  44005  radcnvrat  44310  2reu8i  47118  zm1nn  47307  subsubelfzo0  47331  2ffzoeq  47332  fargshiftf  47445  2pwp1prm  47594  lighneal  47616  isuspgrimlem  47899  upgrimpths  47913  gpgedgvtx0  48056  gpgedgvtx1  48057  isassintop  48202  uzlidlring  48227  2zrngamgm  48237  ply1mulgsumlem1  48379  suppdm  48503  rrxsphere  48741  inlinecirc02plem  48779  pgindnf  49709