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

This theorem is referenced by:  mo4  2560  eqrdav  2731  spc2ed  3591  rexraleqim  3635  disjiun  5135  disjord  5136  disjiund  5138  propeqop  5507  euotd  5513  pwssun  5571  iotan0  6533  funopsn  7145  isotr  7332  funeldmb  7355  funfv1st2nd  8031  funelss  8032  el2mpocsbcl  8070  ressuppssdif  8169  oeordi  8586  domunsncan  9071  pssnn  9167  pssnnOLD  9264  findcard3  9284  findcard3OLD  9285  ordtypelem7  9518  inf3lem5  9626  r1tr  9770  cardmin2  9993  ac10ct  10028  isf32lem12  10358  isfin1-3  10380  fin17  10388  fin1a2s  10408  axdc4lem  10449  axcclem  10451  ttukeylem2  10504  genpcd  11000  ltexprlem3  11032  prlem936  11041  supsrlem  11105  mul0or  11853  un0addcl  12504  un0mulcl  12505  btwnnz  12637  uznfz  13583  elfz0ubfz0  13604  elfzo0z  13673  fzofzim  13678  ssfzoulel  13725  ssfzo12bi  13726  subfzo0  13753  modmuladdim  13878  modaddmodup  13898  modfzo0difsn  13907  axdc4uzlem  13947  expaddz  14071  sq01  14187  hashnn0n0nn  14350  hashss  14368  hashgt12el  14381  fi1uzind  14457  brfi1indALT  14460  ccatalpha  14542  swrdswrdlem  14653  swrdswrd  14654  swrdccatin1  14674  pfxccatin12lem3  14681  repswswrd  14733  cshf1  14759  cshw1  14771  2cshwcshw  14775  sqrmo  15197  caubnd2  15303  summo  15662  nno  16324  divalglem8  16342  lcmdvds  16544  lcmfunsnlem1  16573  hashgcdeq  16721  modprm0  16737  pcqcl  16788  vdwnnlem3  16929  prmgaplem5  16987  prmgaplem7  16989  catpropd  17652  cicsym  17750  isinitoi  17948  istermoi  17949  iszeroi  17958  acsfiindd  18505  tsrlemax  18538  issubg4  19024  gsmsymgreqlem2  19298  oddvdsnn0  19411  oddvds  19414  gexdvds  19451  lt6abl  19762  pgpfac1lem3  19946  01eq0ring  20304  isphld  21206  coe1ae0  21739  mdetdiaglem  22099  slesolex  22183  pmatcoe1fsupp  22202  cpmatelimp  22213  cpmatelimp2  22215  cpmatmcllem  22219  pm2mpf1  22300  mp2pm2mplem4  22310  fvmptnn04ifa  22351  fvmptnn04ifd  22354  chfacfscmul0  22359  chfacfpmmul0  22363  neii1  22609  neii2  22611  uncmp  22906  isfild  23361  fbunfip  23372  fgss2  23377  fgcl  23381  isufil2  23411  cfinufil  23431  ufilen  23433  fsumcn  24385  lmmbr  24774  iscau4  24795  caussi  24813  cmslssbn  24888  ovoliunnul  25023  ovolicc2lem4  25036  itg1ge0a  25228  rolle  25506  ulmcaulem  25905  cxpge0  26190  fsumvma  26713  gausslemma2dlem1a  26865  2sqb  26932  2sq2  26933  pntrsumbnd2  27067  pntlem3  27109  nofv  27157  sltres  27162  axeuclid  28218  axcontlem2  28220  usgrislfuspgr  28441  nbuhgr2vtx1edgblem  28605  usgredgsscusgredg  28713  upgrwlkvtxedg  28899  uspgr2wlkeq  28900  cyclnspth  29054  uspgrn2crct  29059  crctcshwlkn0lem4  29064  wlkiswwlks2lem5  29124  wlknewwlksn  29138  umgrwwlks2on  29208  clwwlkccatlem  29239  clwlkclwwlklem2a4  29247  clwlkclwwlklem2a  29248  clwwisshclwwslemlem  29263  clwwlkel  29296  wwlksubclwwlk  29308  clwwlknon1  29347  clwwlknonex2lem2  29358  uhgr3cyclexlem  29431  vdgn1frgrv3  29547  2wspmdisj  29587  frgrregord013  29645  spansncvi  30900  lnconi  31281  cdj3lem1  31682  metider  32869  prsrcmpltd  34081  gonar  34381  goalr  34383  satffunlem2lem1  34390  finminlem  35198  clsint2  35209  bj-finsumval0  36161  finxpsuclem  36273  pibt2  36293  wl-exeq  36398  phpreu  36467  poimirlem26  36509  poimir  36516  ismtyima  36666  elpaddn0  38666  tendospcanN  39889  nnproddivdvdsd  40861  dvdsexpnn0  41232  rexzrexnn0  41532  unxpwdom3  41827  unielss  41957  onov0suclim  42014  fsovrfovd  42750  radcnvrat  43063  2reu8i  45811  zm1nn  46000  subsubelfzo0  46024  fzoopth  46025  2ffzoeq  46026  fargshiftf  46098  2pwp1prm  46247  lighneal  46269  isomuspgrlem1  46485  isassintop  46610  uzlidlring  46817  2zrngamgm  46827  ply1mulgsumlem1  47057  suppdm  47181  rrxsphere  47424  inlinecirc02plem  47462  pgindnf  47751