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 206  df-an 396

This theorem is referenced by:  mo4  2566  eqrdav  2737  spc2ed  3530  rexraleqim  3569  disjiun  5057  disjord  5058  disjiund  5060  propeqop  5415  euotd  5421  pwssun  5476  iotan0  6408  funopsn  7002  isotr  7187  funfv1st2nd  7860  funelss  7861  el2mpocsbcl  7896  ressuppssdif  7972  oeordi  8380  domunsncan  8812  pssnn  8913  pssnnOLD  8969  findcard3  8987  ordtypelem7  9213  inf3lem5  9320  r1tr  9465  cardmin2  9688  ac10ct  9721  isf32lem12  10051  isfin1-3  10073  fin17  10081  fin1a2s  10101  axdc4lem  10142  axcclem  10144  ttukeylem2  10197  genpcd  10693  ltexprlem3  10725  prlem936  10734  supsrlem  10798  mul0or  11545  un0addcl  12196  un0mulcl  12197  btwnnz  12326  uznfz  13268  elfz0ubfz0  13289  elfzo0z  13357  fzofzim  13362  ssfzoulel  13409  ssfzo12bi  13410  subfzo0  13437  modmuladdim  13562  modaddmodup  13582  modfzo0difsn  13591  axdc4uzlem  13631  expaddz  13755  sq01  13868  hashnn0n0nn  14034  hashss  14052  hashgt12el  14065  fi1uzind  14139  brfi1indALT  14142  ccatalpha  14226  swrdswrdlem  14345  swrdswrd  14346  swrdccatin1  14366  pfxccatin12lem3  14373  repswswrd  14425  cshf1  14451  cshw1  14463  2cshwcshw  14466  sqrmo  14891  caubnd2  14997  summo  15357  nno  16019  divalglem8  16037  lcmdvds  16241  lcmfunsnlem1  16270  hashgcdeq  16418  modprm0  16434  pcqcl  16485  vdwnnlem3  16626  prmgaplem5  16684  prmgaplem7  16686  catpropd  17335  cicsym  17433  isinitoi  17630  istermoi  17631  iszeroi  17640  acsfiindd  18186  tsrlemax  18219  issubg4  18689  gsmsymgreqlem2  18954  oddvdsnn0  19067  oddvds  19070  gexdvds  19104  lt6abl  19411  pgpfac1lem3  19595  isphld  20771  coe1ae0  21297  mdetdiaglem  21655  slesolex  21739  pmatcoe1fsupp  21758  cpmatelimp  21769  cpmatelimp2  21771  cpmatmcllem  21775  pm2mpf1  21856  mp2pm2mplem4  21866  fvmptnn04ifa  21907  fvmptnn04ifd  21910  chfacfscmul0  21915  chfacfpmmul0  21919  neii1  22165  neii2  22167  uncmp  22462  isfild  22917  fbunfip  22928  fgss2  22933  fgcl  22937  isufil2  22967  cfinufil  22987  ufilen  22989  fsumcn  23939  lmmbr  24327  iscau4  24348  caussi  24366  cmslssbn  24441  ovoliunnul  24576  ovolicc2lem4  24589  itg1ge0a  24781  rolle  25059  ulmcaulem  25458  cxpge0  25743  fsumvma  26266  gausslemma2dlem1a  26418  2sqb  26485  2sq2  26486  pntrsumbnd2  26620  pntlem3  26662  axeuclid  27234  axcontlem2  27236  usgrislfuspgr  27457  nbuhgr2vtx1edgblem  27621  usgredgsscusgredg  27729  upgrwlkvtxedg  27914  uspgr2wlkeq  27915  cyclnspth  28069  uspgrn2crct  28074  crctcshwlkn0lem4  28079  wlkiswwlks2lem5  28139  wlknewwlksn  28153  umgrwwlks2on  28223  clwwlkccatlem  28254  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwwisshclwwslemlem  28278  clwwlkel  28311  wwlksubclwwlk  28323  clwwlknon1  28362  clwwlknonex2lem2  28373  uhgr3cyclexlem  28446  vdgn1frgrv3  28562  2wspmdisj  28602  frgrregord013  28660  spansncvi  29915  lnconi  30296  cdj3lem1  30697  metider  31746  prsrcmpltd  32955  gonar  33257  goalr  33259  satffunlem2lem1  33266  funeldmb  33643  nofv  33787  sltres  33792  finminlem  34434  clsint2  34445  bj-finsumval0  35383  finxpsuclem  35495  pibt2  35515  wl-exeq  35620  phpreu  35688  poimirlem26  35730  poimir  35737  ismtyima  35888  elpaddn0  37741  tendospcanN  38964  nnproddivdvdsd  39937  dvdsexpnn0  40262  rexzrexnn0  40542  unxpwdom3  40836  fsovrfovd  41506  radcnvrat  41821  2reu8i  44492  zm1nn  44682  subsubelfzo0  44706  fzoopth  44707  2ffzoeq  44708  fargshiftf  44780  2pwp1prm  44929  lighneal  44951  isomuspgrlem1  45167  isassintop  45292  uzlidlring  45375  2zrngamgm  45385  ply1mulgsumlem1  45615  suppdm  45739  rrxsphere  45982  inlinecirc02plem  46020