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 208  df-an 397

This theorem is referenced by:  mo4  2570  spc2ed  3539  rexraleqim  3585  disjiun  5060  disjord  5061  disjiund  5063  propeqop  5448  euotd  5454  pwssun  5510  iotan0  6475  funopsn  7090  funopsnOLD  7091  isotr  7280  funeldmb  7303  resf1extb  7874  funfv1st2nd  7988  funelss  7989  el2mpocsbcl  8024  ressuppssdif  8125  oeordi  8513  domunsncan  9005  pssnn  9093  findcard3  9183  ordtypelem7  9429  inf3lem5  9544  r1tr  9691  cardmin2  9914  ac10ct  9947  isf32lem12  10277  isfin1-3  10299  fin17  10307  fin1a2s  10327  axdc4lem  10368  axcclem  10370  ttukeylem2  10423  genpcd  10920  ltexprlem3  10952  prlem936  10961  supsrlem  11025  mul0or  11781  un0addcl  12461  un0mulcl  12462  btwnnz  12596  uznfz  13555  elfz0ubfz0  13577  elfzo0z  13647  fzofzim  13655  ssfzoulel  13706  ssfzo12bi  13707  fzoopth  13708  subfzo0  13738  modmuladdim  13867  modaddmodup  13887  modfzo0difsn  13896  axdc4uzlem  13936  expaddz  14059  sq01  14178  hashnn0n0nn  14344  hashss  14362  hashgt12el  14375  fi1uzind  14460  brfi1indALT  14463  ccatalpha  14547  swrdswrdlem  14657  swrdswrd  14658  swrdccatin1  14678  pfxccatin12lem3  14685  repswswrd  14737  cshf1  14763  cshw1  14775  2cshwcshw  14778  sqrmo  15204  caubnd2  15311  summo  15670  nno  16342  divalglem8  16360  lcmdvds  16568  lcmfunsnlem1  16597  hashgcdeq  16751  modprm0  16767  pcqcl  16818  vdwnnlem3  16959  prmgaplem5  17017  prmgaplem7  17019  catpropd  17666  cicsym  17762  isinitoi  17957  istermoi  17958  iszeroi  17967  acsfiindd  18510  tsrlemax  18543  issubg4  19112  gsmsymgreqlem2  19397  oddvdsnn0  19510  oddvds  19513  gexdvds  19550  lt6abl  19861  pgpfac1lem3  20045  01eq0ring  20502  isphld  21629  psdmul  22154  coe1ae0  22201  mdetdiaglem  22581  slesolex  22665  pmatcoe1fsupp  22684  cpmatelimp  22695  cpmatelimp2  22697  cpmatmcllem  22701  pm2mpf1  22782  mp2pm2mplem4  22792  fvmptnn04ifa  22833  fvmptnn04ifd  22836  chfacfscmul0  22841  chfacfpmmul0  22845  neii1  23089  neii2  23091  uncmp  23386  isfild  23841  fbunfip  23852  fgss2  23857  fgcl  23861  isufil2  23891  cfinufil  23911  ufilen  23913  fsumcn  24855  lmmbr  25243  iscau4  25264  caussi  25282  cmslssbn  25357  ovoliunnul  25492  ovolicc2lem4  25505  itg1ge0a  25696  rolle  25975  ulmcaulem  26377  cxpge0  26665  fsumvma  27194  gausslemma2dlem1a  27346  2sqb  27413  2sq2  27414  pntrsumbnd2  27548  pntlem3  27590  nofv  27639  ltsres  27644  muls0ord  28195  axeuclid  29050  axcontlem2  29052  usgrislfuspgr  29274  nbuhgr2vtx1edgblem  29438  usgredgsscusgredg  29546  upgrwlkvtxedg  29731  uspgr2wlkeq  29732  cyclnspth  29887  uspgrn2crct  29894  crctcshwlkn0lem4  29899  wlkiswwlks2lem5  29959  wlknewwlksn  29973  usgrwwlks2on  30044  umgrwwlks2on  30045  clwwlkccatlem  30077  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwwisshclwwslemlem  30101  clwwlkel  30134  wwlksubclwwlk  30146  clwwlknon1  30185  clwwlknonex2lem2  30196  uhgr3cyclexlem  30269  vdgn1frgrv3  30385  2wspmdisj  30425  frgrregord013  30483  spansncvi  31741  lnconi  32122  cdj3lem1  32523  constrsqrtcl  33963  metider  34078  prsrcmpltd  35263  onvf1odlem4  35334  gonar  35623  goalr  35625  satffunlem2lem1  35632  finminlem  36546  clsint2  36557  cgsex2gd  37497  bj-finsumval0  37645  finxpsuclem  37759  pibt2  37779  wl-exeq  37905  phpreu  37971  poimirlem26  38013  poimir  38020  ismtyima  38170  elpaddn0  40292  tendospcanN  41515  nnproddivdvdsd  42485  dvdsexpnn0  42811  sn-remul0ord  42885  rexzrexnn0  43249  unxpwdom3  43540  unielss  43663  onov0suclim  43719  fsovrfovd  44453  radcnvrat  44758  2reu8i  47576  zm1nn  47765  subsubelfzo0  47790  2ffzoeq  47791  nnmul2  47793  fargshiftf  47915  2pwp1prm  48067  lighneal  48089  isuspgrimlem  48386  upgrimpths  48400  clnbgr3stgrgrlim  48510  gpgedgvtx0  48552  gpgedgvtx1  48553  isassintop  48701  uzlidlring  48726  2zrngamgm  48736  ply1mulgsumlem1  48877  suppdm  49001  rrxsphere  49239  inlinecirc02plem  49277  pgindnf  50206