Theorem impancom 455

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 416	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 410	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mo4  2625  eqrdav  2797  spc2ed  3550  rexraleqim  3588  disjiun  5017  disjord  5018  disjiund  5020  propeqop  5362  euotd  5368  pwssun  5421  iotan0  6314  funopsn  6887  isotr  7068  funfv1st2nd  7727  funelss  7728  el2mpocsbcl  7763  ressuppssdif  7834  oeordi  8196  domunsncan  8600  pssnn  8720  findcard3  8745  ordtypelem7  8972  inf3lem5  9079  r1tr  9189  cardmin2  9412  ac10ct  9445  isf32lem12  9775  isfin1-3  9797  fin17  9805  fin1a2s  9825  axdc4lem  9866  axcclem  9868  ttukeylem2  9921  genpcd  10417  ltexprlem3  10449  prlem936  10458  supsrlem  10522  mul0or  11269  un0addcl  11918  un0mulcl  11919  btwnnz  12046  uznfz  12985  elfz0ubfz0  13006  elfzo0z  13074  fzofzim  13079  ssfzoulel  13126  ssfzo12bi  13127  subfzo0  13154  modmuladdim  13277  modaddmodup  13297  modfzo0difsn  13306  axdc4uzlem  13346  expaddz  13469  sq01  13582  hashnn0n0nn  13748  hashss  13766  hashgt12el  13779  fi1uzind  13851  brfi1indALT  13854  ccatalpha  13938  swrdswrdlem  14057  swrdswrd  14058  swrdccatin1  14078  pfxccatin12lem3  14085  repswswrd  14137  cshf1  14163  cshw1  14175  2cshwcshw  14178  sqrmo  14603  caubnd2  14709  summo  15066  nno  15723  divalglem8  15741  lcmdvds  15942  lcmfunsnlem1  15971  hashgcdeq  16116  modprm0  16132  pcqcl  16183  vdwnnlem3  16323  prmgaplem5  16381  prmgaplem7  16383  catpropd  16971  cicsym  17066  isinitoi  17255  istermoi  17256  iszeroi  17261  acsfiindd  17779  tsrlemax  17822  issubg4  18290  gsmsymgreqlem2  18551  oddvdsnn0  18664  oddvds  18667  gexdvds  18701  lt6abl  19008  pgpfac1lem3  19192  isphld  20343  coe1ae0  20845  mdetdiaglem  21203  slesolex  21287  pmatcoe1fsupp  21306  cpmatelimp  21317  cpmatelimp2  21319  cpmatmcllem  21323  pm2mpf1  21404  mp2pm2mplem4  21414  fvmptnn04ifa  21455  fvmptnn04ifd  21458  chfacfscmul0  21463  chfacfpmmul0  21467  neii1  21711  neii2  21713  uncmp  22008  isfild  22463  fbunfip  22474  fgss2  22479  fgcl  22483  isufil2  22513  cfinufil  22533  ufilen  22535  fsumcn  23475  lmmbr  23862  iscau4  23883  caussi  23901  cmslssbn  23976  ovoliunnul  24111  ovolicc2lem4  24124  itg1ge0a  24315  rolle  24593  ulmcaulem  24989  cxpge0  25274  fsumvma  25797  gausslemma2dlem1a  25949  2sqb  26016  2sq2  26017  pntrsumbnd2  26151  pntlem3  26193  axeuclid  26757  axcontlem2  26759  usgrislfuspgr  26977  nbuhgr2vtx1edgblem  27141  usgredgsscusgredg  27249  upgrwlkvtxedg  27434  uspgr2wlkeq  27435  cyclnspth  27589  uspgrn2crct  27594  crctcshwlkn0lem4  27599  wlkiswwlks2lem5  27659  wlknewwlksn  27673  umgrwwlks2on  27743  clwwlkccatlem  27774  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwwisshclwwslemlem  27798  clwwlkel  27831  wwlksubclwwlk  27843  clwwlknon1  27882  clwwlknonex2lem2  27893  uhgr3cyclexlem  27966  vdgn1frgrv3  28082  2wspmdisj  28122  frgrregord013  28180  spansncvi  29435  lnconi  29816  cdj3lem1  30217  metider  31247  prsrcmpltd  32457  gonar  32755  goalr  32757  satffunlem2lem1  32764  funeldmb  33119  nofv  33277  sltres  33282  finminlem  33779  clsint2  33790  bj-finsumval0  34700  finxpsuclem  34814  pibt2  34834  wl-exeq  34939  phpreu  35041  poimirlem26  35083  poimir  35090  ismtyima  35241  elpaddn0  37096  tendospcanN  38319  nnproddivdvdsd  39289  rexzrexnn0  39745  unxpwdom3  40039  fsovrfovd  40710  radcnvrat  41018  2reu8i  43669  zm1nn  43859  subsubelfzo0  43883  fzoopth  43884  2ffzoeq  43885  fargshiftf  43957  2pwp1prm  44106  lighneal  44129  isomuspgrlem1  44345  isassintop  44470  uzlidlring  44553  2zrngamgm  44563  ply1mulgsumlem1  44794  suppdm  44919  rrxsphere  45162  inlinecirc02plem  45200