Theorem impancom 456

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 417	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 411	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mo4  2594  spc2ed  3561  rexraleqim  3607  disjiun  5098  disjord  5099  disjiund  5101  propeqop  5492  euotd  5498  pwssun  5555  iotan0  6528  funopsn  7146  funopsnOLD  7147  isotr  7336  funeldmb  7359  resf1extb  7932  funfv1st2nd  8044  funelss  8045  el2mpocsbcl  8081  ressuppssdif  8182  oeordi  8574  domunsncan  9066  pssnn  9154  findcard3  9244  ordtypelem7  9487  inf3lem5  9602  r1tr  9749  cardmin2  9986  ac10ct  10019  isf32lem12  10349  isfin1-3  10371  fin17  10379  fin1a2s  10399  axdc4lem  10440  axcclem  10442  ttukeylem2  10495  genpcd  10992  ltexprlem3  11024  prlem936  11033  supsrlem  11097  mul0or  11855  un0addcl  12538  un0mulcl  12539  btwnnz  12673  uznfz  13640  elfz0ubfz0  13662  elfzo0z  13732  fzofzim  13740  ssfzoulel  13791  ssfzo12bi  13792  fzoopth  13793  subfzo0  13823  modmuladdim  13952  modaddmodup  13972  modfzo0difsn  13981  axdc4uzlem  14021  expaddz  14144  sq01  14263  hashnn0n0nn  14429  hashss  14447  hashgt12el  14461  fi1uzind  14546  brfi1indALT  14549  ccatalpha  14633  swrdswrdlem  14743  swrdswrd  14744  swrdccatin1  14764  pfxccatin12lem3  14771  repswswrd  14823  cshf1  14849  cshw1  14861  2cshwcshw  14864  sqrmo  15304  caubnd2  15411  summo  15770  nno  16441  divalglem8  16459  lcmdvds  16667  lcmfunsnlem1  16696  hashgcdeq  16850  modprm0  16866  pcqcl  16917  vdwnnlem3  17058  prmgaplem5  17116  prmgaplem7  17118  catpropd  17766  cicsym  17862  isinitoi  18057  istermoi  18058  iszeroi  18067  acsfiindd  18610  tsrlemax  18643  issubg4  19213  gsmsymgreqlem2  19502  oddvdsnn0  19615  oddvds  19618  gexdvds  19655  lt6abl  19966  pgpfac1lem3  20150  01eq0ring  20615  unichnlidl  21343  isphld  21785  psdmul  22310  coe1ae0  22357  mdetdiaglem  22736  slesolex  22820  pmatcoe1fsupp  22839  cpmatelimp  22850  cpmatelimp2  22852  cpmatmcllem  22856  pm2mpf1  22937  mp2pm2mplem4  22947  fvmptnn04ifa  22988  fvmptnn04ifd  22991  chfacfscmul0  22996  chfacfpmmul0  23000  neii1  23244  neii2  23246  uncmp  23541  isfild  23996  fbunfip  24007  fgss2  24012  fgcl  24016  isufil2  24046  cfinufil  24066  ufilen  24068  fsumcn  25010  lmmbr  25398  iscau4  25419  caussi  25437  cmslssbn  25512  ovoliunnul  25647  ovolicc2lem4  25660  itg1ge0a  25851  rolle  26130  ulmcaulem  26538  cxpge0  26829  fsumvma  27358  gausslemma2dlem1a  27510  2sqb  27577  2sq2  27578  pntrsumbnd2  27712  pntlem3  27754  nofv  27802  ltsres  27807  muls0ord  28359  axeuclid  29294  axcontlem2  29296  usgrislfuspgr  29518  nbuhgr2vtx1edgblem  29682  usgredgsscusgredg  29790  upgrwlkvtxedg  29975  uspgr2wlkeq  29976  cyclnspth  30131  uspgrn2crct  30138  crctcshwlkn0lem4  30143  wlkiswwlks2lem5  30203  wlknewwlksn  30217  usgrwwlks2on  30288  umgrwwlks2on  30289  clwwlkccatlem  30321  clwlkclwwlklem2a4  30329  clwlkclwwlklem2a  30330  clwwisshclwwslemlem  30345  clwwlkel  30378  wwlksubclwwlk  30390  clwwlknon1  30429  clwwlknonex2lem2  30440  uhgr3cyclexlem  30513  vdgn1frgrv3  30629  2wspmdisj  30669  frgrregord013  30727  spansncvi  31985  lnconi  32366  cdj3lem1  32767  constrsqrtcl  34150  metider  34265  prsrcmpltd  35451  onvf1odlem4  35571  gonar  35868  goalr  35870  satffunlem2lem1  35877  finminlem  36810  clsint2  36821  cgsex2gd  37762  bj-finsumval0  37910  finxpsuclem  38024  pibt2  38044  wl-exeq  38170  phpreu  38236  poimirlem26  38278  poimir  38285  ismtyima  38435  elpaddn0  40555  tendospcanN  41778  nnproddivdvdsd  42748  dvdsexpnn0  43076  sn-remul0ord  43150  rexzrexnn0  43514  unxpwdom3  43805  unielss  43928  onov0suclim  43984  fsovrfovd  44718  radcnvrat  45007  2reu8i  47833  zm1nn  48022  subsubelfzo0  48047  2ffzoeq  48048  nnmul2  48050  fargshiftf  48172  2pwp1prm  48324  lighneal  48346  isuspgrimlem  48643  upgrimpths  48657  clnbgr3stgrgrlim  48767  gpgedgvtx0  48809  gpgedgvtx1  48810  isassintop  48958  uzlidlring  48983  2zrngamgm  48993  ply1mulgsumlem1  49149  suppdm  49273  rrxsphere  49511  inlinecirc02plem  49549  pgindnf  50477