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  2566  spc2ed  3543  rexraleqim  3589  disjiun  5073  disjord  5074  disjiund  5076  propeqop  5461  euotd  5467  pwssun  5523  iotan0  6488  funopsn  7101  funopsnOLD  7102  isotr  7291  funeldmb  7314  resf1extb  7885  funfv1st2nd  7999  funelss  8000  el2mpocsbcl  8035  ressuppssdif  8135  oeordi  8523  domunsncan  9015  pssnn  9103  findcard3  9193  ordtypelem7  9439  inf3lem5  9553  r1tr  9700  cardmin2  9923  ac10ct  9956  isf32lem12  10286  isfin1-3  10308  fin17  10316  fin1a2s  10336  axdc4lem  10377  axcclem  10379  ttukeylem2  10432  genpcd  10929  ltexprlem3  10961  prlem936  10970  supsrlem  11034  mul0or  11790  un0addcl  12470  un0mulcl  12471  btwnnz  12605  uznfz  13564  elfz0ubfz0  13586  elfzo0z  13656  fzofzim  13664  ssfzoulel  13715  ssfzo12bi  13716  fzoopth  13717  subfzo0  13747  modmuladdim  13876  modaddmodup  13896  modfzo0difsn  13905  axdc4uzlem  13945  expaddz  14068  sq01  14187  hashnn0n0nn  14353  hashss  14371  hashgt12el  14384  fi1uzind  14469  brfi1indALT  14472  ccatalpha  14556  swrdswrdlem  14666  swrdswrd  14667  swrdccatin1  14687  pfxccatin12lem3  14694  repswswrd  14746  cshf1  14772  cshw1  14784  2cshwcshw  14787  sqrmo  15213  caubnd2  15320  summo  15679  nno  16351  divalglem8  16369  lcmdvds  16577  lcmfunsnlem1  16606  hashgcdeq  16760  modprm0  16776  pcqcl  16827  vdwnnlem3  16968  prmgaplem5  17026  prmgaplem7  17028  catpropd  17675  cicsym  17771  isinitoi  17966  istermoi  17967  iszeroi  17976  acsfiindd  18519  tsrlemax  18552  issubg4  19121  gsmsymgreqlem2  19406  oddvdsnn0  19519  oddvds  19522  gexdvds  19559  lt6abl  19870  pgpfac1lem3  20054  01eq0ring  20507  isphld  21634  psdmul  22132  coe1ae0  22180  mdetdiaglem  22563  slesolex  22647  pmatcoe1fsupp  22666  cpmatelimp  22677  cpmatelimp2  22679  cpmatmcllem  22683  pm2mpf1  22764  mp2pm2mplem4  22774  fvmptnn04ifa  22815  fvmptnn04ifd  22818  chfacfscmul0  22823  chfacfpmmul0  22827  neii1  23071  neii2  23073  uncmp  23368  isfild  23823  fbunfip  23834  fgss2  23839  fgcl  23843  isufil2  23873  cfinufil  23893  ufilen  23895  fsumcn  24837  lmmbr  25225  iscau4  25246  caussi  25264  cmslssbn  25339  ovoliunnul  25474  ovolicc2lem4  25487  itg1ge0a  25678  rolle  25957  ulmcaulem  26359  cxpge0  26647  fsumvma  27176  gausslemma2dlem1a  27328  2sqb  27395  2sq2  27396  pntrsumbnd2  27530  pntlem3  27572  nofv  27621  ltsres  27626  muls0ord  28177  axeuclid  29032  axcontlem2  29034  usgrislfuspgr  29256  nbuhgr2vtx1edgblem  29420  usgredgsscusgredg  29528  upgrwlkvtxedg  29713  uspgr2wlkeq  29714  cyclnspth  29869  uspgrn2crct  29876  crctcshwlkn0lem4  29881  wlkiswwlks2lem5  29941  wlknewwlksn  29955  usgrwwlks2on  30026  umgrwwlks2on  30027  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwwisshclwwslemlem  30083  clwwlkel  30116  wwlksubclwwlk  30128  clwwlknon1  30167  clwwlknonex2lem2  30178  uhgr3cyclexlem  30251  vdgn1frgrv3  30367  2wspmdisj  30407  frgrregord013  30465  spansncvi  31723  lnconi  32104  cdj3lem1  32505  constrsqrtcl  33923  metider  34038  prsrcmpltd  35223  onvf1odlem4  35288  gonar  35577  goalr  35579  satffunlem2lem1  35586  finminlem  36500  clsint2  36511  cgsex2gd  37451  bj-finsumval0  37599  finxpsuclem  37713  pibt2  37733  wl-exeq  37859  phpreu  37925  poimirlem26  37967  poimir  37974  ismtyima  38124  elpaddn0  40246  tendospcanN  41469  nnproddivdvdsd  42439  dvdsexpnn0  42766  sn-remul0ord  42840  rexzrexnn0  43232  unxpwdom3  43523  unielss  43646  onov0suclim  43702  fsovrfovd  44436  radcnvrat  44741  2reu8i  47561  zm1nn  47750  subsubelfzo0  47775  2ffzoeq  47776  nnmul2  47778  fargshiftf  47900  2pwp1prm  48052  lighneal  48074  isuspgrimlem  48371  upgrimpths  48385  clnbgr3stgrgrlim  48495  gpgedgvtx0  48537  gpgedgvtx1  48538  isassintop  48686  uzlidlring  48711  2zrngamgm  48721  ply1mulgsumlem1  48862  suppdm  48986  rrxsphere  49224  inlinecirc02plem  49262  pgindnf  50191