Theorem impancom 455

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mo4  2592  spc2ed  3559  rexraleqim  3605  disjiun  5085  disjord  5086  disjiund  5088  propeqop  5473  euotd  5479  pwssun  5535  iotan0  6506  funopsn  7125  funopsnOLD  7126  isotr  7315  funeldmb  7338  resf1extb  7910  funfv1st2nd  8022  funelss  8023  el2mpocsbcl  8058  ressuppssdif  8159  oeordi  8551  domunsncan  9043  pssnn  9131  findcard3  9221  ordtypelem7  9466  inf3lem5  9581  r1tr  9728  cardmin2  9951  ac10ct  9984  isf32lem12  10315  isfin1-3  10337  fin17  10345  fin1a2s  10365  axdc4lem  10406  axcclem  10408  ttukeylem2  10461  genpcd  10958  ltexprlem3  10990  prlem936  10999  supsrlem  11063  mul0or  11821  un0addcl  12508  un0mulcl  12509  btwnnz  12643  uznfz  13609  elfz0ubfz0  13631  elfzo0z  13701  fzofzim  13709  ssfzoulel  13760  ssfzo12bi  13761  fzoopth  13762  subfzo0  13792  modmuladdim  13921  modaddmodup  13941  modfzo0difsn  13950  axdc4uzlem  13990  expaddz  14113  sq01  14232  hashnn0n0nn  14398  hashss  14416  hashgt12el  14429  fi1uzind  14514  brfi1indALT  14517  ccatalpha  14601  swrdswrdlem  14711  swrdswrd  14712  swrdccatin1  14732  pfxccatin12lem3  14739  repswswrd  14791  cshf1  14817  cshw1  14829  2cshwcshw  14832  sqrmo  15269  caubnd2  15376  summo  15735  nno  16407  divalglem8  16425  lcmdvds  16633  lcmfunsnlem1  16662  hashgcdeq  16816  modprm0  16832  pcqcl  16883  vdwnnlem3  17024  prmgaplem5  17082  prmgaplem7  17084  catpropd  17732  cicsym  17828  isinitoi  18023  istermoi  18024  iszeroi  18033  acsfiindd  18576  tsrlemax  18609  issubg4  19178  gsmsymgreqlem2  19462  oddvdsnn0  19575  oddvds  19578  gexdvds  19615  lt6abl  19926  pgpfac1lem3  20110  01eq0ring  20567  isphld  21694  psdmul  22219  coe1ae0  22266  mdetdiaglem  22646  slesolex  22730  pmatcoe1fsupp  22749  cpmatelimp  22760  cpmatelimp2  22762  cpmatmcllem  22766  pm2mpf1  22847  mp2pm2mplem4  22857  fvmptnn04ifa  22898  fvmptnn04ifd  22901  chfacfscmul0  22906  chfacfpmmul0  22910  neii1  23154  neii2  23156  uncmp  23451  isfild  23906  fbunfip  23917  fgss2  23922  fgcl  23926  isufil2  23956  cfinufil  23976  ufilen  23978  fsumcn  24920  lmmbr  25308  iscau4  25329  caussi  25347  cmslssbn  25422  ovoliunnul  25557  ovolicc2lem4  25570  itg1ge0a  25761  rolle  26040  ulmcaulem  26445  cxpge0  26736  fsumvma  27265  gausslemma2dlem1a  27417  2sqb  27484  2sq2  27485  pntrsumbnd2  27619  pntlem3  27661  nofv  27709  ltsres  27714  muls0ord  28266  axeuclid  29121  axcontlem2  29123  usgrislfuspgr  29345  nbuhgr2vtx1edgblem  29509  usgredgsscusgredg  29617  upgrwlkvtxedg  29802  uspgr2wlkeq  29803  cyclnspth  29958  uspgrn2crct  29965  crctcshwlkn0lem4  29970  wlkiswwlks2lem5  30030  wlknewwlksn  30044  usgrwwlks2on  30115  umgrwwlks2on  30116  clwwlkccatlem  30148  clwlkclwwlklem2a4  30156  clwlkclwwlklem2a  30157  clwwisshclwwslemlem  30172  clwwlkel  30205  wwlksubclwwlk  30217  clwwlknon1  30256  clwwlknonex2lem2  30267  uhgr3cyclexlem  30340  vdgn1frgrv3  30456  2wspmdisj  30496  frgrregord013  30554  spansncvi  31812  lnconi  32193  cdj3lem1  32594  constrsqrtcl  34037  metider  34152  prsrcmpltd  35337  onvf1odlem4  35410  gonar  35706  goalr  35708  satffunlem2lem1  35715  finminlem  36639  clsint2  36650  cgsex2gd  37590  bj-finsumval0  37738  finxpsuclem  37852  pibt2  37872  wl-exeq  37998  phpreu  38064  poimirlem26  38106  poimir  38113  ismtyima  38263  elpaddn0  40385  tendospcanN  41608  nnproddivdvdsd  42578  dvdsexpnn0  42904  sn-remul0ord  42978  rexzrexnn0  43342  unxpwdom3  43633  unielss  43756  onov0suclim  43812  fsovrfovd  44546  radcnvrat  44851  2reu8i  47668  zm1nn  47857  subsubelfzo0  47882  2ffzoeq  47883  nnmul2  47885  fargshiftf  48007  2pwp1prm  48159  lighneal  48181  isuspgrimlem  48478  upgrimpths  48492  clnbgr3stgrgrlim  48602  gpgedgvtx0  48644  gpgedgvtx1  48645  isassintop  48793  uzlidlring  48818  2zrngamgm  48828  ply1mulgsumlem1  48969  suppdm  49093  rrxsphere  49331  inlinecirc02plem  49369  pgindnf  50298