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  3564  rexraleqim  3610  disjiun  5090  disjord  5091  disjiund  5093  propeqop  5462  euotd  5468  pwssun  5523  iotan0  6489  funopsn  7102  isotr  7293  funeldmb  7316  resf1extb  7890  funfv1st2nd  8004  funelss  8005  el2mpocsbcl  8041  ressuppssdif  8141  oeordi  8528  domunsncan  9018  pssnn  9109  findcard3  9205  findcard3OLD  9206  ordtypelem7  9453  inf3lem5  9561  r1tr  9705  cardmin2  9928  ac10ct  9963  isf32lem12  10293  isfin1-3  10315  fin17  10323  fin1a2s  10343  axdc4lem  10384  axcclem  10386  ttukeylem2  10439  genpcd  10935  ltexprlem3  10967  prlem936  10976  supsrlem  11040  mul0or  11794  un0addcl  12451  un0mulcl  12452  btwnnz  12586  uznfz  13547  elfz0ubfz0  13569  elfzo0z  13638  fzofzim  13646  ssfzoulel  13697  ssfzo12bi  13698  fzoopth  13699  subfzo0  13726  modmuladdim  13855  modaddmodup  13875  modfzo0difsn  13884  axdc4uzlem  13924  expaddz  14047  sq01  14166  hashnn0n0nn  14332  hashss  14350  hashgt12el  14363  fi1uzind  14448  brfi1indALT  14451  ccatalpha  14534  swrdswrdlem  14645  swrdswrd  14646  swrdccatin1  14666  pfxccatin12lem3  14673  repswswrd  14725  cshf1  14751  cshw1  14763  2cshwcshw  14767  sqrmo  15193  caubnd2  15300  summo  15659  nno  16328  divalglem8  16346  lcmdvds  16554  lcmfunsnlem1  16583  hashgcdeq  16736  modprm0  16752  pcqcl  16803  vdwnnlem3  16944  prmgaplem5  17002  prmgaplem7  17004  catpropd  17646  cicsym  17742  isinitoi  17937  istermoi  17938  iszeroi  17947  acsfiindd  18488  tsrlemax  18521  issubg4  19053  gsmsymgreqlem2  19337  oddvdsnn0  19450  oddvds  19453  gexdvds  19490  lt6abl  19801  pgpfac1lem3  19985  01eq0ring  20415  isphld  21539  psdmul  22029  coe1ae0  22077  mdetdiaglem  22461  slesolex  22545  pmatcoe1fsupp  22564  cpmatelimp  22575  cpmatelimp2  22577  cpmatmcllem  22581  pm2mpf1  22662  mp2pm2mplem4  22672  fvmptnn04ifa  22713  fvmptnn04ifd  22716  chfacfscmul0  22721  chfacfpmmul0  22725  neii1  22969  neii2  22971  uncmp  23266  isfild  23721  fbunfip  23732  fgss2  23737  fgcl  23741  isufil2  23771  cfinufil  23791  ufilen  23793  fsumcn  24737  lmmbr  25134  iscau4  25155  caussi  25173  cmslssbn  25248  ovoliunnul  25384  ovolicc2lem4  25397  itg1ge0a  25588  rolle  25870  ulmcaulem  26279  cxpge0  26568  fsumvma  27100  gausslemma2dlem1a  27252  2sqb  27319  2sq2  27320  pntrsumbnd2  27454  pntlem3  27496  nofv  27545  sltres  27550  muls0ord  28064  axeuclid  28866  axcontlem2  28868  usgrislfuspgr  29090  nbuhgr2vtx1edgblem  29254  usgredgsscusgredg  29363  upgrwlkvtxedg  29548  uspgr2wlkeq  29549  cyclnspth  29704  uspgrn2crct  29711  crctcshwlkn0lem4  29716  wlkiswwlks2lem5  29776  wlknewwlksn  29790  umgrwwlks2on  29860  clwwlkccatlem  29891  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwwisshclwwslemlem  29915  clwwlkel  29948  wwlksubclwwlk  29960  clwwlknon1  29999  clwwlknonex2lem2  30010  uhgr3cyclexlem  30083  vdgn1frgrv3  30199  2wspmdisj  30239  frgrregord013  30297  spansncvi  31554  lnconi  31935  cdj3lem1  32336  constrsqrtcl  33742  metider  33857  prsrcmpltd  35044  onvf1odlem4  35066  gonar  35355  goalr  35357  satffunlem2lem1  35364  finminlem  36279  clsint2  36290  bj-finsumval0  37246  finxpsuclem  37358  pibt2  37378  wl-exeq  37495  phpreu  37571  poimirlem26  37613  poimir  37620  ismtyima  37770  elpaddn0  39767  tendospcanN  40990  nnproddivdvdsd  41961  dvdsexpnn0  42295  sn-remul0ord  42369  rexzrexnn0  42765  unxpwdom3  43057  unielss  43180  onov0suclim  43236  fsovrfovd  43971  radcnvrat  44276  2reu8i  47087  zm1nn  47276  subsubelfzo0  47300  2ffzoeq  47301  fargshiftf  47414  2pwp1prm  47563  lighneal  47585  isuspgrimlem  47868  upgrimpths  47882  gpgedgvtx0  48025  gpgedgvtx1  48026  isassintop  48171  uzlidlring  48196  2zrngamgm  48206  ply1mulgsumlem1  48348  suppdm  48472  rrxsphere  48710  inlinecirc02plem  48748  pgindnf  49678