Theorem impancom 457

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mo4  2594  spc2ed  3559  rexraleqim  3604  prsrcmpltd  4436  disjiun  5096  disjord  5097  disjiund  5099  propeqop  5486  euotd  5493  pwssun  5550  iotan0  6555  iotan0OLD  6556  funopsn  7183  funopsnOLD  7184  isotr  7375  funeldmb  7400  resf1extb  7980  funfv1st2nd  8092  funelss  8093  el2mpocsbcl  8131  ressuppssdif  8240  oeordi  8634  domunsncan  9134  pssnn  9222  findcard3  9312  ordtypelem7  9555  inf3lem5  9670  r1tr  9820  cardmin2  10119  ac10ct  10152  isf32lem12  10481  isfin1-3  10503  fin17  10511  fin1a2s  10531  axdc4lem  10572  axcclem  10574  ttukeylem2  10627  genpcd  11130  ltexprlem3  11162  prlem936  11171  supsrlem  11235  mul0or  11996  un0addcl  12679  un0mulcl  12680  btwnnz  12815  uznfz  13784  elfz0ubfz0  13806  elfzo0z  13876  fzofzim  13884  ssfzoulel  13935  ssfzo12bi  13936  fzoopth  13937  subfzo0  13968  modmuladdim  14097  modaddmodup  14117  modfzo0difsn  14126  axdc4uzlem  14166  expaddz  14289  sq01  14410  hashnn0n0nn  14576  hashss  14594  hashgt12el  14608  fi1uzind  14693  brfi1indALT  14696  ccatalpha  14781  swrdswrdlem  14895  swrdswrd  14896  swrdccatin1  14916  pfxccatin12lem3  14923  repswswrd  14977  cshf1  15003  cshw1  15015  2cshwcshw  15018  sqrmo  15461  caubnd2  15569  summo  15927  nno  16596  divalglem8  16614  lcmdvds  16827  lcmfunsnlem1  16856  hashgcdeq  17011  modprm0  17027  pcqcl  17078  vdwnnlem3  17219  prmgaplem5  17277  prmgaplem7  17279  catpropd  17933  cicsym  18029  isinitoi  18224  istermoi  18225  iszeroi  18234  acsfiindd  18777  tsrlemax  18810  0gisid  18898  issubg4  19406  gsmsymgreqlem2  19696  oddvdsnn0  19809  oddvds  19812  gexdvds  19849  lt6abl  20160  pgpfac1lem3  20344  01eq0ring  20832  unichnlidl  21567  isphld  22015  psdmul  22542  coe1ae0  22589  mdetdiaglem  22968  slesolex  23055  pmatcoe1fsupp  23074  cpmatelimp  23085  cpmatelimp2  23087  cpmatmcllem  23091  pm2mpf1  23172  mp2pm2mplem4  23182  fvmptnn04ifa  23223  fvmptnn04ifd  23226  chfacfscmul0  23231  chfacfpmmul0  23235  neii1  23479  neii2  23481  uncmp  23776  isfild  24232  fbunfip  24243  fgss2  24248  fgcl  24252  isufil2  24282  cfinufil  24302  ufilen  24304  fsumcn  25246  lmmbr  25634  iscau4  25655  caussi  25673  cmslssbn  25748  ovoliunnul  25883  ovolicc2lem4  25896  itg1ge0a  26087  rolle  26365  ulmcaulem  26778  cxpge0  27068  fsumvma  27597  gausslemma2dlem1a  27749  2sqb  27816  2sq2  27817  pntrsumbnd2  27951  pntlem3  27993  nofv  28071  ltsres  28076  muls0ord  28628  axeuclid  29598  axcontlem2  29600  usgrislfuspgr  29825  nbuhgr2vtx1edgblem  29989  usgredgsscusgredg  30097  upgrwlkvtxedg  30282  uspgr2wlkeq  30283  cyclnspth  30446  uspgrn2crct  30454  crctcshwlkn0lem4  30459  wlkiswwlks2lem5  30519  wlknewwlksn  30533  usgrwwlks2on  30604  umgrwwlks2on  30605  clwwlkccatlem  30637  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwwisshclwwslemlem  30661  clwwlkel  30694  wwlksubclwwlk  30706  clwwlknon1  30745  clwwlknonex2lem2  30756  uhgr3cyclexlem  30839  vdgn1frgrv3  30955  2wspmdisj  30995  frgrregord013  31053  spansncvi  32311  lnconi  32692  cdj3lem1  33093  constrsqrtcl  34522  metider  34637  onvf1odlem4  36075  onprcf1acwevdlem1  36086  gonar  36368  goalr  36370  satffunlem2lem1  36377  mirimanoffr  36668  finminlem  37321  clsint2  37332  cgsex2gd  38329  bj-finsumval0  38474  finxpsuclem  38588  pibt2  38608  wl-exeq  38734  phpreu  38795  poimirlem26  38832  poimir  38839  ismtyima  39003  elpaddn0  41123  tendospcanN  42346  nnproddivdvdsd  43316  dvdsexpnn0  43652  sn-remul0ord  43725  rexzrexnn0  44077  unxpwdom3  44363  unielss  44481  onov0suclim  44537  fsovrfovd  45270  radcnvrat  45559  2reu8i  48457  zm1nn  48645  subsubelfzo0  48670  2ffzoeq  48671  nnmul2  48673  fargshiftf  48795  2pwp1prm  48947  lighneal  48969  isuspgrimlem  49266  upgrimpths  49280  clnbgr3stgrgrlim  49390  gpgedgvtx0  49432  gpgedgvtx1  49433  isassintop  49580  uzlidlring  49605  2zrngamgm  49615  ply1mulgsumlem1  49829  suppdm  49953  rrxsphere  50191  inlinecirc02plem  50229  pgindnf  51215