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  2563  eqrdav  2733  spc2ed  3600  rexraleqim  3646  disjiun  5135  disjord  5136  disjiund  5138  propeqop  5516  euotd  5522  pwssun  5579  iotan0  6552  funopsn  7167  isotr  7355  funeldmb  7378  funfv1st2nd  8069  funelss  8070  el2mpocsbcl  8108  ressuppssdif  8208  oeordi  8623  domunsncan  9110  pssnn  9206  findcard3  9315  findcard3OLD  9316  ordtypelem7  9561  inf3lem5  9669  r1tr  9813  cardmin2  10036  ac10ct  10071  isf32lem12  10401  isfin1-3  10423  fin17  10431  fin1a2s  10451  axdc4lem  10492  axcclem  10494  ttukeylem2  10547  genpcd  11043  ltexprlem3  11075  prlem936  11084  supsrlem  11148  mul0or  11900  un0addcl  12556  un0mulcl  12557  btwnnz  12691  uznfz  13646  elfz0ubfz0  13668  elfzo0z  13737  fzofzim  13745  ssfzoulel  13795  ssfzo12bi  13796  fzoopth  13797  subfzo0  13824  modmuladdim  13951  modaddmodup  13971  modfzo0difsn  13980  axdc4uzlem  14020  expaddz  14143  sq01  14260  hashnn0n0nn  14426  hashss  14444  hashgt12el  14457  fi1uzind  14542  brfi1indALT  14545  ccatalpha  14627  swrdswrdlem  14738  swrdswrd  14739  swrdccatin1  14759  pfxccatin12lem3  14766  repswswrd  14818  cshf1  14844  cshw1  14856  2cshwcshw  14860  sqrmo  15286  caubnd2  15392  summo  15749  nno  16415  divalglem8  16433  lcmdvds  16641  lcmfunsnlem1  16670  hashgcdeq  16822  modprm0  16838  pcqcl  16889  vdwnnlem3  17030  prmgaplem5  17088  prmgaplem7  17090  catpropd  17753  cicsym  17851  isinitoi  18052  istermoi  18053  iszeroi  18062  acsfiindd  18610  tsrlemax  18643  issubg4  19175  gsmsymgreqlem2  19463  oddvdsnn0  19576  oddvds  19579  gexdvds  19616  lt6abl  19927  pgpfac1lem3  20111  01eq0ring  20546  isphld  21689  psdmul  22187  coe1ae0  22233  mdetdiaglem  22619  slesolex  22703  pmatcoe1fsupp  22722  cpmatelimp  22733  cpmatelimp2  22735  cpmatmcllem  22739  pm2mpf1  22820  mp2pm2mplem4  22830  fvmptnn04ifa  22871  fvmptnn04ifd  22874  chfacfscmul0  22879  chfacfpmmul0  22883  neii1  23129  neii2  23131  uncmp  23426  isfild  23881  fbunfip  23892  fgss2  23897  fgcl  23901  isufil2  23931  cfinufil  23951  ufilen  23953  fsumcn  24907  lmmbr  25305  iscau4  25326  caussi  25344  cmslssbn  25419  ovoliunnul  25555  ovolicc2lem4  25568  itg1ge0a  25760  rolle  26042  ulmcaulem  26451  cxpge0  26739  fsumvma  27271  gausslemma2dlem1a  27423  2sqb  27490  2sq2  27491  pntrsumbnd2  27625  pntlem3  27667  nofv  27716  sltres  27721  muls0ord  28225  axeuclid  28992  axcontlem2  28994  usgrislfuspgr  29218  nbuhgr2vtx1edgblem  29382  usgredgsscusgredg  29491  upgrwlkvtxedg  29677  uspgr2wlkeq  29678  cyclnspth  29832  uspgrn2crct  29837  crctcshwlkn0lem4  29842  wlkiswwlks2lem5  29902  wlknewwlksn  29916  umgrwwlks2on  29986  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwwisshclwwslemlem  30041  clwwlkel  30074  wwlksubclwwlk  30086  clwwlknon1  30125  clwwlknonex2lem2  30136  uhgr3cyclexlem  30209  vdgn1frgrv3  30325  2wspmdisj  30365  frgrregord013  30423  spansncvi  31680  lnconi  32061  cdj3lem1  32462  metider  33854  prsrcmpltd  35073  gonar  35379  goalr  35381  satffunlem2lem1  35388  finminlem  36300  clsint2  36311  bj-finsumval0  37267  finxpsuclem  37379  pibt2  37399  wl-exeq  37514  phpreu  37590  poimirlem26  37632  poimir  37639  ismtyima  37789  elpaddn0  39782  tendospcanN  41005  nnproddivdvdsd  41981  dvdsexpnn0  42347  rexzrexnn0  42791  unxpwdom3  43083  unielss  43206  onov0suclim  43263  fsovrfovd  43998  radcnvrat  44309  2reu8i  47062  zm1nn  47251  subsubelfzo0  47275  2ffzoeq  47276  fargshiftf  47364  2pwp1prm  47513  lighneal  47535  isuspgrimlem  47811  gpgedgvtx0  47953  gpgedgvtx1  47954  isassintop  48053  uzlidlring  48078  2zrngamgm  48088  ply1mulgsumlem1  48231  suppdm  48355  rrxsphere  48597  inlinecirc02plem  48635  pgindnf  48946