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  2560  eqrdav  2731  spc2ed  3591  rexraleqim  3635  disjiun  5135  disjord  5136  disjiund  5138  propeqop  5507  euotd  5513  pwssun  5571  iotan0  6533  funopsn  7148  isotr  7335  funeldmb  7358  funfv1st2nd  8034  funelss  8035  el2mpocsbcl  8073  ressuppssdif  8172  oeordi  8589  domunsncan  9074  pssnn  9170  pssnnOLD  9267  findcard3  9287  findcard3OLD  9288  ordtypelem7  9521  inf3lem5  9629  r1tr  9773  cardmin2  9996  ac10ct  10031  isf32lem12  10361  isfin1-3  10383  fin17  10391  fin1a2s  10411  axdc4lem  10452  axcclem  10454  ttukeylem2  10507  genpcd  11003  ltexprlem3  11035  prlem936  11044  supsrlem  11108  mul0or  11856  un0addcl  12507  un0mulcl  12508  btwnnz  12640  uznfz  13586  elfz0ubfz0  13607  elfzo0z  13676  fzofzim  13681  ssfzoulel  13728  ssfzo12bi  13729  subfzo0  13756  modmuladdim  13881  modaddmodup  13901  modfzo0difsn  13910  axdc4uzlem  13950  expaddz  14074  sq01  14190  hashnn0n0nn  14353  hashss  14371  hashgt12el  14384  fi1uzind  14460  brfi1indALT  14463  ccatalpha  14545  swrdswrdlem  14656  swrdswrd  14657  swrdccatin1  14677  pfxccatin12lem3  14684  repswswrd  14736  cshf1  14762  cshw1  14774  2cshwcshw  14778  sqrmo  15200  caubnd2  15306  summo  15665  nno  16327  divalglem8  16345  lcmdvds  16547  lcmfunsnlem1  16576  hashgcdeq  16724  modprm0  16740  pcqcl  16791  vdwnnlem3  16932  prmgaplem5  16990  prmgaplem7  16992  catpropd  17655  cicsym  17753  isinitoi  17951  istermoi  17952  iszeroi  17961  acsfiindd  18508  tsrlemax  18541  issubg4  19027  gsmsymgreqlem2  19301  oddvdsnn0  19414  oddvds  19417  gexdvds  19454  lt6abl  19765  pgpfac1lem3  19949  01eq0ring  20309  isphld  21213  coe1ae0  21746  mdetdiaglem  22107  slesolex  22191  pmatcoe1fsupp  22210  cpmatelimp  22221  cpmatelimp2  22223  cpmatmcllem  22227  pm2mpf1  22308  mp2pm2mplem4  22318  fvmptnn04ifa  22359  fvmptnn04ifd  22362  chfacfscmul0  22367  chfacfpmmul0  22371  neii1  22617  neii2  22619  uncmp  22914  isfild  23369  fbunfip  23380  fgss2  23385  fgcl  23389  isufil2  23419  cfinufil  23439  ufilen  23441  fsumcn  24393  lmmbr  24782  iscau4  24803  caussi  24821  cmslssbn  24896  ovoliunnul  25031  ovolicc2lem4  25044  itg1ge0a  25236  rolle  25514  ulmcaulem  25913  cxpge0  26198  fsumvma  26723  gausslemma2dlem1a  26875  2sqb  26942  2sq2  26943  pntrsumbnd2  27077  pntlem3  27119  nofv  27167  sltres  27172  axeuclid  28259  axcontlem2  28261  usgrislfuspgr  28482  nbuhgr2vtx1edgblem  28646  usgredgsscusgredg  28754  upgrwlkvtxedg  28940  uspgr2wlkeq  28941  cyclnspth  29095  uspgrn2crct  29100  crctcshwlkn0lem4  29105  wlkiswwlks2lem5  29165  wlknewwlksn  29179  umgrwwlks2on  29249  clwwlkccatlem  29280  clwlkclwwlklem2a4  29288  clwlkclwwlklem2a  29289  clwwisshclwwslemlem  29304  clwwlkel  29337  wwlksubclwwlk  29349  clwwlknon1  29388  clwwlknonex2lem2  29399  uhgr3cyclexlem  29472  vdgn1frgrv3  29588  2wspmdisj  29628  frgrregord013  29686  spansncvi  30943  lnconi  31324  cdj3lem1  31725  metider  32943  prsrcmpltd  34155  gonar  34455  goalr  34457  satffunlem2lem1  34464  finminlem  35289  clsint2  35300  bj-finsumval0  36252  finxpsuclem  36364  pibt2  36384  wl-exeq  36489  phpreu  36558  poimirlem26  36600  poimir  36607  ismtyima  36757  elpaddn0  38757  tendospcanN  39980  nnproddivdvdsd  40952  dvdsexpnn0  41314  rexzrexnn0  41624  unxpwdom3  41919  unielss  42049  onov0suclim  42106  fsovrfovd  42842  radcnvrat  43155  2reu8i  45900  zm1nn  46089  subsubelfzo0  46113  fzoopth  46114  2ffzoeq  46115  fargshiftf  46187  2pwp1prm  46336  lighneal  46358  isomuspgrlem1  46574  isassintop  46699  uzlidlring  46906  2zrngamgm  46916  ply1mulgsumlem1  47145  suppdm  47269  rrxsphere  47512  inlinecirc02plem  47550  pgindnf  47839