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 206  df-an 396

This theorem is referenced by:  mo4  2559  eqrdav  2730  spc2ed  3591  rexraleqim  3635  disjiun  5135  disjord  5136  disjiund  5138  propeqop  5507  euotd  5513  pwssun  5571  iotan0  6533  funopsn  7148  isotr  7336  funeldmb  7359  funfv1st2nd  8035  funelss  8036  el2mpocsbcl  8074  ressuppssdif  8173  oeordi  8590  domunsncan  9075  pssnn  9171  pssnnOLD  9268  findcard3  9288  findcard3OLD  9289  ordtypelem7  9522  inf3lem5  9630  r1tr  9774  cardmin2  9997  ac10ct  10032  isf32lem12  10362  isfin1-3  10384  fin17  10392  fin1a2s  10412  axdc4lem  10453  axcclem  10455  ttukeylem2  10508  genpcd  11004  ltexprlem3  11036  prlem936  11045  supsrlem  11109  mul0or  11859  un0addcl  12510  un0mulcl  12511  btwnnz  12643  uznfz  13589  elfz0ubfz0  13610  elfzo0z  13679  fzofzim  13684  ssfzoulel  13731  ssfzo12bi  13732  subfzo0  13759  modmuladdim  13884  modaddmodup  13904  modfzo0difsn  13913  axdc4uzlem  13953  expaddz  14077  sq01  14193  hashnn0n0nn  14356  hashss  14374  hashgt12el  14387  fi1uzind  14463  brfi1indALT  14466  ccatalpha  14548  swrdswrdlem  14659  swrdswrd  14660  swrdccatin1  14680  pfxccatin12lem3  14687  repswswrd  14739  cshf1  14765  cshw1  14777  2cshwcshw  14781  sqrmo  15203  caubnd2  15309  summo  15668  nno  16330  divalglem8  16348  lcmdvds  16550  lcmfunsnlem1  16579  hashgcdeq  16727  modprm0  16743  pcqcl  16794  vdwnnlem3  16935  prmgaplem5  16993  prmgaplem7  16995  catpropd  17658  cicsym  17756  isinitoi  17954  istermoi  17955  iszeroi  17964  acsfiindd  18511  tsrlemax  18544  issubg4  19062  gsmsymgreqlem2  19341  oddvdsnn0  19454  oddvds  19457  gexdvds  19494  lt6abl  19805  pgpfac1lem3  19989  01eq0ring  20420  isphld  21427  coe1ae0  21960  mdetdiaglem  22321  slesolex  22405  pmatcoe1fsupp  22424  cpmatelimp  22435  cpmatelimp2  22437  cpmatmcllem  22441  pm2mpf1  22522  mp2pm2mplem4  22532  fvmptnn04ifa  22573  fvmptnn04ifd  22576  chfacfscmul0  22581  chfacfpmmul0  22585  neii1  22831  neii2  22833  uncmp  23128  isfild  23583  fbunfip  23594  fgss2  23599  fgcl  23603  isufil2  23633  cfinufil  23653  ufilen  23655  fsumcn  24609  lmmbr  25007  iscau4  25028  caussi  25046  cmslssbn  25121  ovoliunnul  25257  ovolicc2lem4  25270  itg1ge0a  25462  rolle  25743  ulmcaulem  26143  cxpge0  26428  fsumvma  26953  gausslemma2dlem1a  27105  2sqb  27172  2sq2  27173  pntrsumbnd2  27307  pntlem3  27349  nofv  27397  sltres  27402  axeuclid  28489  axcontlem2  28491  usgrislfuspgr  28712  nbuhgr2vtx1edgblem  28876  usgredgsscusgredg  28984  upgrwlkvtxedg  29170  uspgr2wlkeq  29171  cyclnspth  29325  uspgrn2crct  29330  crctcshwlkn0lem4  29335  wlkiswwlks2lem5  29395  wlknewwlksn  29409  umgrwwlks2on  29479  clwwlkccatlem  29510  clwlkclwwlklem2a4  29518  clwlkclwwlklem2a  29519  clwwisshclwwslemlem  29534  clwwlkel  29567  wwlksubclwwlk  29579  clwwlknon1  29618  clwwlknonex2lem2  29629  uhgr3cyclexlem  29702  vdgn1frgrv3  29818  2wspmdisj  29858  frgrregord013  29916  spansncvi  31173  lnconi  31554  cdj3lem1  31955  metider  33173  prsrcmpltd  34385  gonar  34685  goalr  34687  satffunlem2lem1  34694  finminlem  35507  clsint2  35518  bj-finsumval0  36470  finxpsuclem  36582  pibt2  36602  wl-exeq  36707  phpreu  36776  poimirlem26  36818  poimir  36825  ismtyima  36975  elpaddn0  38975  tendospcanN  40198  nnproddivdvdsd  41173  dvdsexpnn0  41535  rexzrexnn0  41845  unxpwdom3  42140  unielss  42270  onov0suclim  42327  fsovrfovd  43063  radcnvrat  43376  2reu8i  46120  zm1nn  46309  subsubelfzo0  46333  fzoopth  46334  2ffzoeq  46335  fargshiftf  46407  2pwp1prm  46556  lighneal  46578  isomuspgrlem1  46794  isassintop  46887  uzlidlring  46916  2zrngamgm  46926  ply1mulgsumlem1  47155  suppdm  47279  rrxsphere  47522  inlinecirc02plem  47560  pgindnf  47849